<div dir="ltr"><div><div><div><div><div><div><div>Hi Yves,<br><br></div>Currently, as far as I am aware, there is no documentation or tutorials on how to program with CakeML.<br></div>However, I hope there will be some day soon. More concretely, I have plans to help write a book on using CakeML early next year.<br><br></div>In the meantime, playing around and asking questions on the mailing list is very welcome.<br></div>Currently, I think the only way to run version 2 of the compiler is by rewriting its definition in the logic, following the script in compiler/eval/example/example.sml.<br>To run version 1, however, you can simply download it from the CakeML website and follow the simple instructions there.<br></div><div>We hope to produce an executable REPL of version 2 of the compiler within a month or two.<br></div><div><br></div>Programming in CakeML can be very much like programming in Standard ML. However, to produce verified programs with CakeML (which is its intended strength) there are two main approaches, and the first is slightly different from normal unverified programming. The approaches are: 1. Write your program as a function in HOL, verify it as usual, and use the HOL-to-CakeML translator to produce the verified implementation in CakeML; or 2. Write your program in CakeML directly, then use the CakeML-to-HOL translator (which currently does not exist) to produce characteristic formulae over which you can verify your program in HOL.<br><br></div>I'm very sorry I cannot point you to documentation yet, but I hope I will be able to later.<br></div><div><br>Ramana<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 1 May 2016 at 10:42, Yves Cloutier <span dir="ltr"><<a href="mailto:yves.cloutier@gmail.com" target="_blank">yves.cloutier@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Hello, <br><br></div>I would like to know if there is ducomentation or tutorials on how to program with CakeML?<br><br></div>Regards,<br><br></div>yves<br></div>
<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" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
<br></blockquote></div><br></div>