[CakeML] Learning material for CakeML

[Mario Castelán Castro]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170918/b06ab285/attachment.asc>