Baking for Dafny: A CakeML Backend for Dafny
Daniel Nezamabadi, Magnus Myreen

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsData Quality and Management
