[CakeML] CakeML User Guide / Tutorial

[Ramana Kumar]

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.

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.
If you're interested in the verification part, then learning HOL or
Isabelle would also make sense.
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.)

On 2 May 2016 at 00:48, Yves Cloutier <yves.cloutier at gmail.com> wrote:

> 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/20160502/8ec93d17/attachment.html>