Dafny vs. Dala: Experience with Mechanising Language Design
James Noble, Julian Mackay, Tobias Wrigstad, Andrew Fawcet, Michael Homer · 2024
Dala is a design for a concurrent dynamic object-oriented language. A key goal of Dala's design is to avoid data races, by ensuring threads do not share mutable state. In this paper we discuss our experience using the program verification tool Dafny to validate Dala's design. We explain how we modelled salient features of Dala in Dafny, and how Dafny did (or did not) assist our confidence in Dala's design.