<div dir="ltr">Good luck with the writing. Like Freek, I'd be happy to comment on drafts.<div><br></div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jan 28, 2014 at 6:02 AM, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@cl.cam.ac.uk" target="_blank">magnus.myreen@cl.cam.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On 28 January 2014 08:18, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>

> On Mon, Jan 27, 2014 at 10:45 AM, Konrad Slind <<a href="mailto:konrad.slind@gmail.com">konrad.slind@gmail.com</a>> wrote:<br>
>>   First, congratulations Ramana for the excellent talk at POPL. I thought it<br>
>> was very well received.<br>
><br>
> Thank you!<br>
><br>
>>  Scott and I talked about how to get standalone executables that I can prove<br>
>> properties about at the HOL function level. He reckoned that if the<br>
>> functions<br>
>> were small enough, I could just run the compiler inside the logic, obtain<br>
>> the<br>
>> bytecodes, run the bytecode compiler (if that's what it is) and get the x86.<br>
>> I would then need to write my own small C wrapper that initalized the cakeML<br>
>> runtime system such that the relevant properties it needs are satisfied.<br>
>> Then<br>
>> jump to the compiled code and run.<br>
>><br>
>>   If that's not a bad idea (seemed plausible to me) I will get started on<br>
>> that for<br>
>> some small programs to see whether it is possible.<br>
><br>
> Indeed that does sound like a good idea. The first step is getting a<br>
> CakeML version of your program, which is the job of the translator.<br>
> You can see how this is done for QSORT in<br>
> translator/ml_translator_demoScript.sml. Once you have the certified<br>
> CakeML program, then you can either run the compiler on it in the<br>
> logic or run it in the (as-yet-non-existent) compiler outside the<br>
> logic. I'll be happy to work with you on making that work (both ways<br>
> eventually, but at least the first way) after submitting to ITP.<br>
><br>
>><br>
>>  I will still need to get the system built. I would also like to get the<br>
>> REPL built<br>
>> so that I can play with it. What is the status of that?<br>
><br>
> I'll let Magnus answer, since he has been working on it most recently.<br>
<br>
</div></div>I'm also in a hurry to get ready for the ITP deadline. The status of<br>
the machine-code implementation is that it's incomplete, due to a few<br>
remaining cheats in the proof and a few bugs I've found in the<br>
underlying x86 model. I'll update you as soon as there's news<br>
regarding the implementation.<br>
<br>
Cheers,<br>
Magnus<br>
<div class="HOEnZb"><div class="h5"><br>
>><br>
>> Thanks,<br>
>> Konrad.<br>
>><br>
>><br>
>><br>
>> _______________________________________________<br>
>> Users mailing list<br>
>> <a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
>> <a href="https://lists.cakeml.org/listinfo/users" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
>><br>
><br>
> _______________________________________________<br>
> Users mailing list<br>
> <a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/users" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
</div></div></blockquote></div><br></div>