<div dir="ltr">Hi all,<div><br></div><div>  First, congratulations Ramana for the excellent talk at POPL. I thought it</div><div>was very well received.</div><div><br></div><div> Scott and I talked about how to get standalone executables that I can prove</div>
<div>properties about at the HOL function level. He reckoned that if the functions </div><div>were small enough, I could just run the compiler inside the logic, obtain the</div><div>bytecodes, run the bytecode compiler (if that's what it is) and get the x86. </div>
<div>I would then need to write my own small C wrapper that initalized the cakeML</div><div>runtime system such that the relevant properties it needs are satisfied. Then</div><div>jump to the compiled code and run.</div><div>
<br></div><div>  If that's not a bad idea (seemed plausible to me) I will get started on that for</div><div>some small programs to see whether it is possible.</div><div><br></div><div> I will still need to get the system built. I would also like to get the REPL built</div>
<div>so that I can play with it. What is the status of that?</div><div><br></div><div>Thanks,</div><div>Konrad.</div><div><br></div><div><br></div></div>