The Pancake Project

Pancake is a new 'thin' language constructed with the aims of (1) ease of source-level verification, (2) user-controlled small memory footprint, and (3) simple transportation of correctness results from source to executable binary code. The Pancake compiler builds on the lower parts of the CakeML compiler.

Motivation

Several people have expressed interest in an imperative space-constrained language (no GC, no dynamic memory allocation) built on the CakeML compiler. We have claimed that infrastructure in the CakeML compiler can be used to implement other compilers. Pancake is our answer.

The Pancake Language

Name. Originally, the name Pancake stood for "Pascal-like language based on the lower half of CakeML compiler". However, the Pascal part should not be taken too seriously. Instead, the language can be seen as mix between a portable assembly language with structured control-flow and an untyped C-like language, but, unlike either of those, Pancake has a straightforward and verification friendly (low-level) semantics.

Why is Pancake untyped? Type systems for languages like C are a way to establish some basic safety properties. Pancake is untyped because programmers might not like to be tied down to a type system. The basic safety properties provided by a type system seem pointless in the context of Pancake programs that are intended for proofs of functional correctness. The functional correctness properties that one proves for Pancake programs imply the basic safety properties that type systems can provide.

Values. Pancake programs consist of a collection of (possibly mutually recursive) functions. These functions take multiple arguments and return multiple values. Local variables hold source values that consist of machine words or tuples/structs of source values, i.e. nested tuples/structs are supported. Structs/tuples held in local variables are stored in registers and/or the stack.

Memory. The language is built to be very explicit about memory usage. Heap memory usage is completely controlled by the programmer. Stack usage is something the compiler determines and is explicit about. If the user refrains from non-tail-recursive recursion, then the compiler will output the number of machine words of stack space that the program can at most use. This number is a proved-correct upper bound on stack usage.

Tools for Pancake

Two tools are currently under development for Pancake:

State of development: the compiler is almost complete; the extractor is still work-in-progress.

Contact

Get in touch with Magnus Myreen with questions. Alternatively, ask questions about Pancake in the public CakeML slack.