Idris - Systems Programming Meets Full Dependent Types
Presenter: Mehmet
Preview
Mehmet will demonstrate use of dependent types for writing and verifying systems programs. He will be presenting “Idris - Systems Programming Meets Full Dependent Types” by Edwin Brady.
Summary
The paper presents a nice framework to build parsers for network packets with proof requirements to demonstrate how dependent types can be used for systems programming. Throughout the examples, the paper shows how to build a safer FFI and how to derive the plain functions from FFI definitions using partial evaluation and the type system. It also demonstrates how to encode validity proof requirements into data structure specifications and how to combine macros and the tactic language to automatize search for proofs of previous dynamic checks happening. During the presentation, we tried to try out some of the examples but got sidetracked because of dramatic changes to Idris (including syntax, new behavior of the totality checker, and change in type names) in the past 6 years. Although the paper gave a nice framework for safer systems programming, the usual problem of “are we proving the right thing?” was still there. The described safer FFI design methodology relied on artificially imposing some of the requirements on top of more “raw” FFI declarations which left a slightly unpleasant feeling. Also, we were surprised and sad about Idris not doing totality checks anymore.