Proofware

(Remember, proofs are programs!)

An important part of my time is devoted to designing, writing and proving software, as well as techniques to do all these things. The programs that I am interested in themselves prove things about formal artifacts: other programs, logic formulas, mathematical theorems, etc. Some of these systems, such as proof assistants and automated theorem provers, can directly offer formal guarantees by connecting a formalized program specification with its verified implementation. Others, like programming languages and their compilers, can themselves be verified and impart indirectly, by way of their specification, certain guarantees to the programs they manipulate, such as correctness of translation or useful security properties.

  • Secure compilers protect compiled programs and the high-level invariants of their source languages against adversarial low-level code that may attempt to subvert those guarantees. We seek to develop such compilers and proof techniques for realistic languages, focusing in particular in compartmentalization techniques for systems languages such as C, and efficient enforcement based on hardware mechanisms, in particular micropolicy machines.

  • I have given plenty of thought to the internals of proof assistants, in particular to Abella, both in relatively self-contained but useful features and technical improvements, and in large, ongoing modifications to the kernel of the system. More broadly, I work on the design of elegant and programmable tactical languages for proof automation, extending their applicability to the Coq proof assistant.

  • Many smaller projects are directly related to the declared goal of ProofCert of universal production, communication (i.e., reuse) and checking (i.e., trust) of proof evidence. Families of proof checkers (minimalistic or not, correct by construction or certified), as well as foundational proof certificate formats, belong here.

  • During the summer of 2016, I prototyped a gradually typed flavor of the Ruby programming language, similar in spirit to recent developments for other dynamic languages — though my various other projects have kept me from revisiting it. The original proposal was supported by the Google Summer of Code program.

  • … and more!

Some of this work is publicly available as free and open source software, while more experimental, embryonic projects patiently bide their time.

Previously, I have worked as a software engineer building and maintaining complex software systems for insurance, as well as built high-performance scientific computing systems for bioinformatics applications, among others. All these experiences inform my understanding of what computer systems are and what they can be, not only conceptually but also in practice.