Type Theory for The Working Rustacean
Venue: Rust Belt Rust 2019
Rust really hits a sweet spot with respect to programming languages on account of a) its usefulness when working at a low level, coupled with b) its style of type system. Because of a), Rust can be—and is—used in places which tend to safety-critical: cyber-physical systems, autonomous vehicle infrastructure, robotics, etc. When building systems for these safety-critical environments, one also often formally proves properties about their software. That’s where b) comes in.
Proof Theory Impressionism: Blurring the Curry-Howard Line
Venue: Strangeloop 2018
The Curry-Howard Correspondence is the observation that there exists a correspondence between objects present in disparate formal systems. Once such instance of this correspondence is the conspicuous propositions-as-types notion, which draws correspondences between logical propositions and types in a programming language.