[CakeML] CakeML User Guide / Tutorial

[Yves Cloutier]

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.

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?

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.

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.

Looking forward to your book, please continue with your work and hope more
contributors join in on your efforts!

Regards,

yves

On Sun, May 1, 2016 at 2:14 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> Hi Yves,
>
> Currently, as far as I am aware, there is no documentation or tutorials on
> how to program with CakeML.
> 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.
>
> In the meantime, playing around and asking questions on the mailing list
> is very welcome.
> 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.
> To run version 1, however, you can simply download it from the CakeML
> website and follow the simple instructions there.
> We hope to produce an executable REPL of version 2 of the compiler within
> a month or two.
>
> 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.
>
> I'm very sorry I cannot point you to documentation yet, but I hope I will
> be able to later.
>
> Ramana
>
> On 1 May 2016 at 10:42, Yves Cloutier <yves.cloutier at gmail.com> wrote:
>
>> Hello,
>>
>> I would like to know if there is ducomentation or tutorials on how to
>> program with CakeML?
>>
>> Regards,
>>
>> yves
>>
>> _______________________________________________
>> Users mailing list
>> Users at cakeml.org
>> https://lists.cakeml.org/listinfo/users
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20160501/403a11b7/attachment.html>