On The Web
A simple modal editor for ascii diagrams featuring shift-drag line drawing and box editing.
A type system for chialisp based on the type theory papers "Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types" and "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" by Jana Dunfield and Neelakantan R. Krishnaswami along with a partial implementation of their algorithm by Kwanghoon Choi.
Code
I'm what might be called a habitual coder. I'm somewhat prolific, and I tend to write an eclectic mix of stuff depending on my interests at the time.
Some highlights
October 5, 2021
My work with chia has yielded a new compiler for the chialisp language, chia's answer to solidity as a language for contracts. The new compiler reorganizes code generation into distinct phases that make adding features to the language less risky and easier, along with providing better diagnostics and source-level debug information to make tracing execution easier.Recently, I've been focused on learing formal proofs, and using proof code for practcal purposes
April 23, 2021
A container library with the proven propery of unique keys.April 22, 2021
This helps code make full use of DecEq and boolean in idris, allowing one to safely transform the "No" case in decidable to a proof of the opposite when it relates to a proof of two boolean expression being equal.I spent a few years working in elm, and getting into the groove of more formal functional programming languages.
June 23, 2017
A lightbox editor in elm that overlays an image on html to make precise alignment easier. Pretty happy with how it turned out.June 19, 2016
An experiment with elm-native-ui to port to 0.17 and remove the need for native js in the module. It turned out well.clang-tooling-style
May 26, 2015
In another life I wrote a lot of C++ and refactored large unruly code. I came up with this:
A style enforcer for a very disciplined flavor of C++ requiring the use of interfaces and dependency injection.
2004-2010
Back in the day, I wrote a lot of code in ReactOS, including most of the code in afd.sys and tcpip.sys.2003
In the prehistory of our century, I was interested in language interoperability and wrote a SWIG module for OCaml.