Colouring flags with Dafny & Idris

Tools

de Muijnck-Hughes, Jan and Noble, James (2024) Colouring flags with Dafny & Idris. In: Dafny 2024, 2024-01-14 - 2024-01-14, Institution of Engineering and Technology. (https://popl24.sigplan.org/details/dafny-2024-pape...)

[thumbnail of de Muijnck-Hughes-Noble-Dafny-2024-Colouring-flags-with-Dafny-&-Idris]
Preview
 Text. Filename: de_Muijnck-Hughes-Noble-Dafny-2024-Colouring-flags-with-Dafny-_-Idris.pdf
Accepted Author Manuscript
License: Strathprints license 1.0
Download (1MB)| Preview

Abstract

Dafny and Idris are two verification-aware programming languages that support two different styles of fine-grained reasoning about our software programs. Dafny is an imperative design-by-contract language that provides a clear separation between specifications and code, while Idris is a dependently-typed functional language in which specifications are code. Each of these approaches support different styles of verification (Hoare Logic in Dafny versus Dependent Type Theory in Idris). In this paper, we will examine how Dafny and Idris express The Problem of the Dutch National Flag from Dijkstra’s Discipline of Programming and note the differences and similarities between both approaches.

ORCID iDs

de Muijnck-Hughes, Jan ORCID logoORCID: https://orcid.org/0000-0003-2185-8543 and Noble, James;
CORE (COnnecting REpositories)