<div dir="ltr"><div><div><div><div><div><div>Thank you for your reply Ramana.  I do understand that CakeML is a work of love and that contributors are working on it on their own time.  But this coming together and collaborating on a shared vision is what makes such initiatives so wonderful.<br><br></div>I guess I should also have asked whether CakeML was suitable for general purpose programming, or if it is geared more towards mathematical and academic audiences?<br><br></div>I'm still very new to functional programming and I guess it would be wise for me to get comfortable with SML before venturing into unknown territory.  <br><br></div>Other functional languages I glanced at were Idris, Mercury, Ur/Web, and of course Haskell and OCaml.  But I have yet to settle on one to learn in depth.  Idris and UR/Web are also very interesting.  It's through this survey of functional languages that I stumbled on CakeML.<br><br></div>Looking forward to your book, please continue with your work and hope more contributors join in on your efforts!<br><br></div>Regards,<br><br></div>yves<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, May 1, 2016 at 2:14 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@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 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"><div><div class="h5">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></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><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></div></div>_______________________________________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">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>
</blockquote></div><br></div>