[CakeML] Learning material for CakeML

Magnus Myreen magnus.myreen at gmail.com
Tue Sep 19 06:15:51 UTC 2017


Hi Mario,

> How should I begin to learn to use CakeML?

The best way is to try to do a small project. Your idea to do a file
compressor (and decompressor) sounds like a good project. I suggest
you start with the simplest possible compressor function (e.g. one
that just inserts "macros" for repeated characters using some escape
character/byte). Once such a toy compressor is proved correct, then
you can move to more serious compressors.

I suggest the following steps:

 1. define compression and decompression as normal HOL functions that
    operate over a list of bytes (word8 from wordsTheory)

 2. prove:  ∀input. decompress (compress input) = input

 3. then use the CakeML translator to turn your functions compress and
    decompress into CakeML code; the translator automatically proves
    that the generated CakeML code has the same behaviour

 4. finally, to make a full application that that can read input and
    write output, you'll need to use the CakeML CF framework (ask for
    advice when you get to this point) and then apply the verified
    compiler to the finished source program

I also suggest that you make your own fork of the CakeML development
on github and develop this example in your version under
characteristic/examples/ so that the example can be easily merged into
the main CakeML repository through a pull request once the example is
finished.

By the way, the CakeML slack might be a good way to ask the
developers questions on CakeML and HOL related topics:

https://join.slack.com/t/cakeml/shared_invite/MjM1NjEyODgxODkzLTE1MDQzNjgwMTUtYjI4YTdlM2VmMQ

Kind regards,
Magnus


On Mon, 18 Sep 2017 at 20:56, Mario Castelán Castro
<marioxcc.MT at yandex.com> wrote:
>
> On 17/09/17 16:04, Magnus Myreen wrote:
> > You can find examples of verified programs in the following directory.
> > These programs range from very simple hello-world programs to Unix-style
> > grep, patch and diff programs.
> >
> > https://github.com/CakeML/cakeml/tree/master/characteristic/examples
> >
> > To understand these script files you'll need to know HOL4 quite well and
> > also understand what the relevant CakeML tools do, e.g. the translator and
> > the CF framework (and later how to apply the compiler).
> >
> > For us to help you get started, it might be good to know more about your
> > aims. Could you tell us what kind of programs you are interested in
> > verifying? Do you have some example in mind? What is your background?
>
> Hello. Thanks for your reply.
>
> As for concrete applications, what I have in mind is to write and
> verifying a file compressor and a computer program to generate canonical
> names of chemical structures. If there is any useful product, it will be
> published as free (as in freedom) software. However, my interest is not
> just a particular project; I am interesting in learning the skill of
> formally-verified programming.
>
> As for my background. I have familiarity with propositional and first
> order logic, and set theory. I have limited experience with HOL4. To
> acquire some practice I have proved some very elementary theorems about
> topology in HOL4. My script file of that is just 174 lines long after
> comments and blank lines have been removed. Regarding functional
> programming I know Common Lisp and some Haskell.
>
> How should I begin to learn to use CakeML?
>
> Regards.
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users



More information about the Users mailing list