| Language | |
| Verbose | |
| Typecheck Only | |
| Unsafe | |
| Unsafe Assertion Checking | |
| Dump Typed Syntax Tree | |
| Dump IR | |
| Dump CFG | |
| Dump WAT |
v24.03.1
About
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:
- Abstract Syntax Tree: Static and Dynamic Semantics are formalised.
- Typechecker: Output is verified to be a well-typed program where all variables are initialised before use and all control-flow paths return. Though, the output hasn't been verified to be correct with respect to the dynamic semantics.
- Typed Syntax Tree: Static Semantics are definitionally enforced. Here is documentation of the static semantics.
- WebAssembly: Static Semantics are formalised; Dynamic Semantics are partially formalised.
Hopefully more will be finished soon! : )
Contributing
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.