Colouring flags with Dafny & Idris

Research output: Contribution to conferencePaperpeer-review

26 Downloads (Pure)


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.
Original languageEnglish
Publication statusPublished - 14 Jan 2024
EventDafny 2024 - Institution of Engineering and Technology, London, United Kingdom
Duration: 14 Jan 202414 Jan 2024


ConferenceDafny 2024
Country/TerritoryUnited Kingdom
Internet address


  • Idris
  • Dafny
  • verification
  • dependent types


Dive into the research topics of 'Colouring flags with Dafny & Idris'. Together they form a unique fingerprint.

Cite this