[CakeML] Verifying CakeML programs

[Magnus Myreen]

Hi Gergely,

> upon reading
>
> https://cakeml.org/popl14.pdf

You'll find a a more up-to-date description here:

https://cakeml.org/icfp16.pdf

> I see that the CakeML system is a verified implementation of the CakeML
> language, where the compiler is not written in CakeML (yet), but it is
> directly encoded as higher order logic formulae.

We automatically generate a CakeML implementation of CakeML compiler.
This was done for version 1 (POPL'14) and is part of the bootstrapping
of the compiler that the POPL paper is talking about. For version 2
(ICFP'16), bootstrapping is not yet complete; we are working on it
right now.

> And, it is not a program verification system for CakeML programs (yet).
>
> Is the above correct? Will there be an extension where I can verify CakeML
> programs, down to machine code?

Yes. For the last 5 months Armaël Guéneau has been visiting Chalmers
(where I'm based) and has formalised Arthur Charguéraud's
characteristic formula (CF) technology for CakeML. You can read more
about CFML here:

http://www.chargueraud.org/softs/cfml/

CakeML's CF framework is very new and has not been used on serious
examples yet. I expect the CF program verification system for CakeML
to become practically usable in the next 3-4 months.

Cheers,
Magnus