Colouring flags with Dafny & Idris

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.