[CakeML] Verifying CakeML programs
magnus.myreen at gmail.com
Thu Aug 11 07:51:42 UTC 2016
> upon reading
You'll find a a more up-to-date description here:
> 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
> 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:
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.
More information about the Users