<div dir="ltr"><div><div>I would say that CakeML is intended to be suitable for general purpose programming. It may not be quite there yet, but that is the goal. The aim is to make it easy to build trustworthy high-quality software for real systems, not just for academics. But our starting point is highly mathematical compared to what the average programmer might be used to these days.<br><br></div>Learning SML or OCaml or Haskell first (it doesn't really matter which one, for a beginner) would be a very good step towards learning CakeML.<br></div><div>If you're interested in the verification part, then learning HOL or Isabelle would also make sense.<br></div>Idris and Ur/Web are also interesting, and take a different approach to verification (based on dependent types). (Agda and Coq are also in this category.)<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 2 May 2016 at 00:48, 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><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="HOEnZb"><div class="h5"><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>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><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>
</div></div></blockquote></div><br></div>