[CakeML] Verifying CakeML programs

Gergely Buday buday.gergely at uni-eszterhazy.hu
Thu Aug 11 07:25:22 UTC 2016


upon reading


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.

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?

- Gergely

More information about the Users mailing list