Dafny vs. Dala: Experience with Mechanising Language Design
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.
Authors
- Michael Homer (ORCID: https://orcid.org/0000-0003-0280-6748)
- Tobias Wrigstad (ORCID: https://orcid.org/0000-0002-4269-5408)
- Julian Mackay (ORCID: https://orcid.org/0000-0003-3098-3901)
- James Noble (ORCID: https://orcid.org/0000-0001-9036-5692)
- Andrew Fawcet
Institutions
- Australian National University (AU)
- Uppsala University (SE)
- Victoria University of Wellington (NZ)
Publication Details
- Published
- 2024-09-13
- DOI
- https://doi.org/10.1145/3678721.3686228
- Citations
- 3
- Primary Topic
- Logic, programming, and type systems
- Type
- article
- Field-Weighted Citation Impact
- 1.04