Colouring Flags with Dafny and Idris - Dafny'24
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
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.
Syllabus
[Dafny'24] Colouring Flags with Dafny & Idris
Taught by
ACM SIGPLAN
Related Courses
You Are a Program SynthesizerStrange Loop Conference via YouTube RustProof: Static Analysis Using MIR - PDXRust October 2016
Rust via YouTube Calculational Design of Correctness and Incorrectness Transformational Program Logics by Abstract Interpretation
ACM SIGPLAN via YouTube The Landscape of Formal Verification in APL - A Review with a Case Study in Quantum Computing
ACM SIGPLAN via YouTube Hyper Hoare Logic: Proving and Disproving Program Hyperproperties
ACM SIGPLAN via YouTube