CakeML is a fully-verified functional programming language. We can use this language, along with a chunk of theorem-proving using the HOL4 system, to generate machine code that we know is absolutely correct (bug-free!).
If you’d like to write code in a functional language (think: Haskell, OCaml, …) and want to know it’s right when you’ve done, talk to me. The details of what we try to develop will be up for discussion, but the possibilities are near-endless (from verifying certain flavours of machine learning algorithm, to Unix command-line utilities, to mathematical algorithms).
- Good knowledge of a functional language (e.g., Haskell), and logic.