[CakeML] Standalones

[Magnus Myreen]

On 28 January 2014 08:18, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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.

I'm also in a hurry to get ready for the ITP deadline. The status of
the machine-code implementation is that it's incomplete, due to a few
remaining cheats in the proof and a few bugs I've found in the
underlying x86 model. I'll update you as soon as there's news
regarding the implementation.

Cheers,
Magnus

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