[CakeML] Verifying CakeML programs
buday.gergely at uni-eszterhazy.hu
Thu Aug 11 07:25:22 UTC 2016
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?
More information about the Users