Ramana.Kumar at cl.cam.ac.uk
Mon Jan 27 21:18:19 UTC 2014
On Mon, Jan 27, 2014 at 10:45 AM, Konrad Slind <konrad.slind at gmail.com> wrote:
> First, congratulations Ramana for the excellent talk at POPL. I thought it
> was very well received.
> Scott and I talked about how to get standalone executables that I can prove
> properties about at the HOL function level. He reckoned that if the
> were small enough, I could just run the compiler inside the logic, obtain
> bytecodes, run the bytecode compiler (if that's what it is) and get the x86.
> I would then need to write my own small C wrapper that initalized the cakeML
> runtime system such that the relevant properties it needs are satisfied.
> jump to the compiled code and run.
> If that's not a bad idea (seemed plausible to me) I will get started on
> that for
> some small programs to see whether it is possible.
Indeed that does sound like a good idea. The first step is getting a
CakeML version of your program, which is the job of the translator.
You can see how this is done for QSORT in
translator/ml_translator_demoScript.sml. Once you have the certified
CakeML program, then you can either run the compiler on it in the
logic or run it in the (as-yet-non-existent) compiler outside the
logic. I'll be happy to work with you on making that work (both ways
eventually, but at least the first way) after submitting to ITP.
> I will still need to get the system built. I would also like to get the
> REPL built
> so that I can play with it. What is the status of that?
I'll let Magnus answer, since he has been working on it most recently.
> Users mailing list
> Users at cakeml.org
More information about the Users