[CakeML] Standalones

[Ramana Kumar]

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.

Thank you!

>  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
> functions
> were small enough, I could just run the compiler inside the logic, obtain
> the
> 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.
> Then
> 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.

>
> Thanks,
> Konrad.
>
>
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>