Colouring Flags with Dafny and Idris - Dafny'24

Explore a comparative analysis of Dafny and Idris in solving The Problem of the Dutch National Flag from Dijkstra's Discipline of Programming. Delve into this 19-minute conference talk presented by Jan de Muijnck-Hughes and James Noble at ACM SIGPLAN's Dafny'24 event. Examine the contrasting approaches of these verification-aware programming languages: Dafny's imperative design-by-contract style with clear separation between specifications and code, and Idris' dependently-typed functional approach where specifications are code. Gain insights into the different verification styles supported by each language, with Dafny utilizing Hoare Logic and Idris employing Dependent Type Theory. Discover the similarities and differences in how these languages express and solve the classic algorithmic problem, providing a deeper understanding of their respective strengths in software verification.