[CakeML] Verifying CakeML programs

[Gergely Buday]

Hi,

upon reading

https://cakeml.org/popl14.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.

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