Getting Started

This page collects advice and links to learning material that we hope help newcomers get started with CakeML, including material about the HOL4 theorem prover where CakeML is developed.

Why CakeML?

Here are some reasons contributors have liked working on CakeML:

CakeML related projects tend to be a fun mix of interactive theorem proving, semantics of functional programming, compiler hacking, and research in programming languages.
The community around CakeML is friendly and supportive. CakeML Discord is a quick way to get advice remotely. There are opportunities to get face-to-face help from CakeML experts at Chalmers Sweden, ANU Australia and NTU Singapore.
Many contributors (particularly MSc students) like working on CakeML because that way their work contributes to a larger, well known, long-running project. Successful CakeML related projects tend to lead to research papers.

Who is this for?

Working on CakeML requires some familiarity with functional programming and reasoning in a formal logic. However, beyond those restrictions, we encourage anyone from students and hobbyists to academics and industry professionals to contribute to CakeML development or to use CakeML.

How to get started?

We suggest following these steps:

Step 1: Look through this web page

The first step is to have a read of what's going on in the CakeML project. The projects page lists and links to on-going and past CakeML related projects. The GitHub issue trackers (for CakeML and for PureCake) offer some insights into anything from minor planned improvements to plans for major new directions.

Step 2: Say hi on Discord (or via email)

We highly encourage everyone involved in CakeML to be part of Discord. It is particularly important to communicate with the established CakeML developers (see the list of currently most active developers) in case you plan to contribute in order to get early feedback on ideas and to get to know how to join on-going efforts.

Step 3: Learn to use the HOL4 theorem prover

CakeML lives in the HOL4 theorem prover. This means that some fluency in using HOL4 is needed in order to work with CakeML. It usually takes a few weeks before newcomers are able to made decent progress in HOL4 scripts. We suggest:

Installing Poly/ML and HOL4
Setting up an editor for HOL4 interaction: emacs, vim or VS Code
Watching: (video links will appear here)
- How to interact with HOL4
- How a small theory is developed
- How to use Holmake and work with several files
- How a small compiler can be verified
- ... and other tutorial videos
Reading the HOL4 tutorial and doing its exercises.
Checking and keeping this cheatsheet close.

Once you've done the above, the best way to make progress is probably to jump in and attempt to do some real proof development, so go ahead and start the real work.

Step 4: Work on your CakeML related thing and keep in touch

While working on your CakeML related project, let us know how it's going by keeping in touch.