Iowa Type Theory Commute

Latest Episodes:

Start of Season 4: Formal Methods for Blockchain Nov 07, 2022

Show notes

I start off a new chapter (seventeen!) of the podcast, to talk about formal methods for blockchain systems. In the next few episodes, we will look at some verification efforts related to the Tezos blockchain.

Separation Logic II: recursive predicates Sep 15, 2022

Show notes

I discuss separation logic basics some more, as presented in the seminal paper by John C. Reynolds. An important idea is describing data structure using separating conjunction and recursive predicates.

Separation Logic 1 Jul 24, 2022

Show notes

I discuss separation logic, as presented in this seminal paper by the great John C. Reynolds. I did not go very far into the topic, so please expect a follow-up episode.

Let's talk about Rust Jul 09, 2022

Show notes

In this episode, I talk briefly about Rust, which uses compile-time analysis to ensure that code is memory-safe (and also free of data races in concurrent code) without using a garbage collector. Fantastic! The language draws on but richly develops ideas on ownership that originated in academic research.

Region-Based Memory Management Jun 21, 2022

Show notes

I discuss the idea of statically typed region-based memory management, proposed by Tofte and Talpin. The idea is to allow programmers to declare explicitly the region from which to satisfy individual allocation requests. Regions are created in a statically scoped way, so that after execution leaves the body of the region-creation construct, the entire region may be deallocated. Type inference is used to make sure that no dangling pointers are dereferenced (after the associated region is deallocated). This journal paper about the idea is not easy reading, but has a lot of good explanations in and around all the technicalities. Even better, I found, is this paper about region-based memory management in Cyclone. There are lots of intuitive explanations of the ideas, and not so much gory technicality.

Introduction to verified memory management Jun 04, 2022

Show notes

In this episode, I start a new chapter (we are up to Chapter 16, here), about verifying safe manual management of memory. I have personally gotten pretty interested in this topic, having seen through some simple experiments with Haskell how much time can go into garbage collection for seemingly simple benchmarks. I also talk about why verifying memory-usage properties of programs is challenging in proof assistants.

More on Metamath May 20, 2022

Show notes

I laud the Metamath proof checker and its excellent book. I am also looking for suggestions on what to discuss next, as I am ready to wrap up this chapter on proof assistants.

Metamath Apr 23, 2022

Show notes

In this episode I share my initial impressions -- very positive! -- of the Metamath system. Metamath allows one to develop theorems from axioms which you state. Typing or other syntactic requirements of axioms or theorems are also expressed axiomatically. The system exhibits an elegant coherent vision for how such a tool should work, and was super easy to download and try out.

The Seventeen Provers of the World Apr 09, 2022

Show notes

I discuss a book edited by Freek Wiedijk (pronounced "Frake Weedike"), which describes the solutions he received in response to a call for formalized proofs of the irrationality of the square root of 2. The book was published in 2006, and made an impression on me then. The provers we have discussed so far all have a solution in the book, except for Lean, which was created after that year. Happily, you can find a PDF of the book here, on Wiedijk's web site.

More on Lean Mar 12, 2022

Show notes

I talk about my positive experience trying out the tools for Lean, specifically the 'lean' executable and lean-mode in emacs.