Typecheck Only
Unsafe Assertion Checking
Dump Typed Syntax Tree
Dump IR
Dump CFG
Dump WAT



C0deine is a compiler for C0. It is written in Lean 4, which allows us to express the formal semantics in the same language as the compiler itself. Hopefully, the whole compiler will be verified at some point/soon.

C0deine implements a number of sub-languages of C0 as well as fixing some bugs in the existing compiler. See this document for information about the languages themselves, as well as a list of changes/corrections. If you find any issues, please report them here.

Verification Status

Currently the following parts of the compiler are verified:

Hopefully more will be finished soon! : )


There is a lot of features, tools, etc. that I would like to implement but not enough hours to work on them. So, if you are interested in contributing please reach out! Even if you are new to Lean there are places that you can help out (so long as you are willing to learn).

Aside about using Lean

Something I found noteworthy about learning Lean was how easy the jump from Standard ML and OCaml to Lean was. From what I've seen, if I have a working function in SML/OCaml, all I really need to do is change the keywords (and annotate the function args/return type) and it generally just works without fuss. Even proofs about SML code can (in my experience) be one-to-one translated into the same proof about the Lean version of the code.

There's a lot more about Lean that I like (how readable it is, tooling, meta-programming, etc.) but I won't go into more depth here. In general, I would like to make it clear that Lean markets itself as a "programming language and theorem prover", but the "theorem proving" part is largely optional. And when evaluating it as a programming language, I struggle to find a reason, other than legacy code and perhaps more existing libraries, to use SML or OCaml over Lean.