CakeML
CakeML is an ML language which supports a subset of SML. It has a correctness theorem that end-to-end verifies that the input provided to the REPL only allows for valid outputs.
The language is written in HOL4, a theorem proving language,
Jul 20, 20251 min read
CakeML is an ML language which supports a subset of SML. It has a correctness theorem that end-to-end verifies that the input provided to the REPL only allows for valid outputs.
The language is written in HOL4, a theorem proving language,