CakeML: A verified implementation of ML

[nickpsecurity]

The best thing since FLINT. My scheme here was to piggy back on it by implementing fast, compatible DSL of CakeML in Racket or something. Do prototyping and testing with fast one. Once ready, compile functions with verified one. Works best for tools that will still have acceptable performance or run in batches overnight. Implement it on Verisoft stack if still available for down to CPU correctness.

Also, some recent threads are on trustworthy compilers with verified vs reproducible builds. The ML languages have made robust compilers much easier to write. One can use this one for that to further reduce TCB and make compiler still easier to write vs C or whatever.

[e12e]

> The best thing since FLINT.

I assume you mean something related to?:

http://flint.cs.yale.edu/flint/software.html

I can't seem to find anything directly related to the software part - is SML/NJ a verified implementation of ML'97?

I was exposed to a bit of Standard ML in university, and it always felt "nicer" than OCaml - but also less practical for actually getting anything done (probably because more people actually write real software in OCaml than in SML?).

As for Racket and SML, I came across the following existing projects:

"This is the Standard ML language embeded in PLT Scheme.": http://planet.racket-lang.org/display.ss?package=sml.plt&own...

"A Standard ML to Racket Translator without type inferencing and checking": https://github.com/stslxg/sml-racket

And while I like the concept of Racket (I've yet to play with it as much as I think it deserves), why not simply use SML/NJ or MLTON if CakeML is a subset of SML? Or possibly implement a non-verfied implementation either on top of MLTON/SML/NJ, or in ML? Curious about your line of thinking there.

[vosper]

> A long-term goal is to make proof assistants into trustworthy and practical program development and implementation platforms. The CakeML compiler verification is an example of proof-assistant-based development; specifically, of proven-correct synthesis of machine code from higher-order logic specifications.

Is CakeML intended to be used to make things, or is it more of a proof of concept?

[poppingtonic]

One of the research organizations using CakeML is MIRI (Machine Intelligence Research Institute), which is doing research in machine self-reference. They recently used HOL, an automated theorem prover, to demonstrate a formal correspondence between the model of HOL within HOL (“inner HOL”) and HOL itself (“outer HOL”). Informally speaking, Fallenstein and Kumar show that one can always build an interpretation of terms in inner HOL such that they have the same meaning as terms in outer HOL. The authors then show that if statements of a certain kind are provable in HOL’s model of itself, they are true in (outer) HOL. See more here: https://intelligence.org/2015/12/04/new-paper-proof-producin...

[gillygize]

"practical program development" implies that it is intended to make things and is not just proof of concept, no?

[Ericson2314]

I'm sorry, but why do people still use HOL? It seems so much more annoying than type-theoretic approaches (Coq/Agda/Idris/Lean). [Cool work judging from the title nevertheless.]

[adrianN]

Different strokes for different folks.

[mafribe]

HOL is a classical rather than constructive logic.

Moreover, there is less concern about soundness of the logic.

[nickpsecurity]

I remember they used to say it was a sound and strong logic vs others.

[julian_1]

Awesome. If anyone knows about this project - how easy would would it be to re-target the backend code generator for something other than x86 or ARM?

[sanxiyn]

It's reasonably retargetable. If you look under compiler/targets in the repository, you will find MIPS and RISC-V backends.