<div dir="ltr"><div><div><div>I think (4) is better in the long run too. The TCB is smaller than (2). Isabelle already ships with binaries, so I think it would make sense to include a verified CakeML binary for this functionality.<br><br></div>For using s-expressions, running the encoder in Isabelle (after OpenTheory translation) as Magnus suggested seems like a good idea to me. As Scott mentioned, you don't need to know the s-expression format exactly (though it's quite simple): what matters is that there are verified encode and decode functions. In particular, there are the theorems topsexp_sexptop and sexptop_topsexp in fromSexpTheory.<br><br></div>The fromSexpTheory doesn't seem to depend on much except astTheory (which you already would have a copy of from your Lem -> Isabelle translation of the CakeML semantics), and simpleSexpTheory (of which it only depends on the sexp datatype - you could define that yourself in Isabelle manually very simply). There is some work on importing OpenTheory packages into Isabelle here:<br><a href="https://github.com/xrchz/isabelle-opentheory">https://github.com/xrchz/isabelle-opentheory</a><br><br></div>To record the fromSexpTheory into OpenTheory format, I think you just need to build it in the otknl.<br><div><div><div><br></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 3 April 2017 at 13:46, Lars Hupel <span dir="ltr"><<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">> I don’t think I can debug this problem :) For what it’s worth, I’m<br>
> using HOL commit be4ab1074df7a6a68bb532146f9bd1<wbr>5b51364344 which is<br>
> pretty recent. You could try that for now.<br>
<br>
</span>That commit fails with the exact same error. I'll take this to<br>
[hol-info] :-)<br>
<div><div class="h5"><br>
> It depends a bit on what kind of assurance story you want to tell. I<br>
> can see a few approaches:<br>
><br>
> 1) Translating the CakeML compiler to SML via the unverified HOL4 SML<br>
> extraction. The TCB includes the unverified translation and PolyML.<br>
><br>
> 2) Translating the CakeML compiler to CakeML via the verified<br>
> translator, and then installing some compatibility libraries to run<br>
> the generated code on PolyML. The TCB is just the compatibility<br>
> libraries and PolyML. The compatibility libraries will have simple<br>
> code, but there are some differences that can’t be handled with a<br>
> library (such as evaluation order and the semantics of polymorphic<br>
> equality). However, those shouldn’t be observable in code produced by<br>
> the translator (this observation is something else being trusted).<br>
><br>
> 3) Translate the CakeML compiler to CakeML and bootstrap it. Now you<br>
> have to produce CakeML concrete syntax to be parsed back in. You are<br>
> trusting your CakeML pretty printer, but not PolyML. If you wrote the<br>
> pretty printer in HOL4, and extracted that using the same techniques<br>
> from 1) and 2), then you could verify the pretty printing algorithm<br>
> and increase assurance, but that would not be a fun proof to do.<br>
><br>
> 4) Translate and bootstrap the compiler, but use the alternate<br>
> s-expression syntax (as Magnus mentioned). The same as 3, but the<br>
> pretty printer is simpler and already verified.<br>
><br>
> The difficulty of getting there from where we are now is (easiest to<br>
> hardest) 3, 4, 2, 1.<br>
><br>
> If you do want a separate bootstrapped executable, then we should<br>
> build that for you as a release, because running the bootstrap takes<br>
> 2 days and needs a computer with lots of RAM.<br>
<br>
</div></div>For now I'd be happy with (4). Of course, eventually this<br>
should be shipped with Isabelle so a source-based distribution model<br>
(i.e. (2)) would be preferable.<br>
<br>
Cheers<br>
<span class="HOEnZb"><font color="#888888">Lars<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
<br>
______________________________<wbr>_________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/users</a><br>
</div></div></blockquote></div><br></div>