“K&R meets ML” (pun courtesy of Graydon).

KReMLin implements the compilation scheme of Low*, i.e. it translates F* programs that are valid Low* into readable C. Readable C is of particular importance for software practicioners (e.g. Mozilla) to read, understand and trust our code. KReMLin extends the Low* theory, and will compile data types & pattern matches, monomorphize polymorphic functions, eliminate unused arguments, simplify data types, and apply many more passes to enhance the quality of the generated C code. Importantly, KReMLin has a set of options that make up a mini DSL to get rid of abstraction and modularity, in favor of tight, compact self-contained C files, a must-have in an actual software project.

KReMLin is open-source, and lives on GitHub.

Verified software

  • I am driving the EverCrypt project, in collaboration with INRIA and CMU and a large subset of Project Everest members.
  • I am a core contributor to HACL*.
  • I also contribute to miTLS.

Thunderbird addons

I was a core contributor, peer and module owner of Thunderbird for several years. During this time, I contributed numerous patches to Thunderbird, along with several add-ons. Amazingly, with the help of contributors, these addons have been running for nearly ten years now.

  • Thunderbird Conversations offers a conversation view for Thunderbird. The addon is a large piece of code and replaces the message reader in Thunderbird. Thunderbird Conversations is on GitHub, and is chiefly maintained by Mark Banner nowadays.
  • Thunderbird Stdlib was an attempt at a standard library for addons, providing reference implementations for complicated tasks (e.g. assemble and send an HTML email).
  • Manually Sort Folders is now the most popular addon. The name is self-explanatory, and the addon is available on GitHub.
  • Latex It! runs Latex on your computer, and transforms $x$ in your email body into the corresponding rendered image. The addon is also on GitHub.

BBC micro:bit hacking

I did a few fun hardware projects with the BBC micro:bit. Here’s some cursory instructions for creating a clock / temperature display; you can also live-stream sensor data from the micro:bit to your javascript web page over usb (very rough instructions).