Baking for Dafny: A CakeML Backend for Dafny

TL;DR

This paper introduces a verified backend translating Dafny programs into CakeML within HOL4, aiming to reduce the trusted computing base by ensuring correctness through formal semantics.

Contribution

It presents the development of a verified Dafny-to-CakeML backend and formal semantics for the Dafny IR to enhance correctness guarantees.

Findings

Successfully implemented a verified translation from Dafny to CakeML.

Formalized big-step semantics for the Dafny intermediate representation.

Reduced the trusted computing base of Dafny's compilation process.

Abstract

Dafny is a verification-aware programming language that allows developers to formally specify their programs and prove them correct. Currently, a Dafny program is compiled in two steps: First, a backend translates the input program to a high-level target language like C# or Rust. Second, the translated program is compiled using the target language's toolchain. Recently, an intermediate representation (IR) has been added to Dafny that serves as input to new backends. At the time of writing, none of these steps are verified, resulting in both the backend and the target language's toolchain being part of Dafny's trusted computing base (TCB). To reduce Dafny's TCB, we started developing a new backend that translates Dafny to CakeML, a verified, bootstrapped subset of Standard ML, in the interactive theorem prover HOL4. We also started to define functional big-step semantics for the Dafny IR to prove correctness of the backend.