I appreciate Theodore Ehrenborg's comments.

As a wee lad, I heard about mathematical certainty of computer programs. Let's go over what I currently believe and don’t believe.

First: what is formal verification 

Sometimes you get pwned because of the spec-implementation gap. The computer did not do what it should’ve done. Other times, you get pwned by the world-spec gap. The computer wasn’t wrong, your “shoulds” were.

Expanding the domain of compiletime knowledge

A compiler tells you the problem with your code when it is, in some sense, “wrong”. When you can define the sense in which your code can be “wrong”, you have circumscribed some domain of compiletime knowledge. In other words, you’ve characterized the kinds of things you can know at compiletime.

The less you know at compiletime, the more you find out at runtime. The less you can afford to wait till [...]

---

Outline:

(00:25) First: what is formal verification

(00:44) Expanding the domain of compiletime knowledge

(01:29) Isolating the bug surface to the world-spec gap, or sidechannels

(02:10) Exploiting inductive structure

(03:50) What I do not say

(04:00) Specify what you want

(04:42) Prove that the AI is correct

(05:56) TLDR, this whole genre of point the formal methods at the learned component itself is viewed by me as a nonstarter.

(06:13) What I do say

(06:20) Swiss cheese!

(07:24) Infrastructure hardening!

(08:30) Boxing/interfaces!

(09:29) Conclusion

The original text contained 3 footnotes which were omitted from this narration.

---

First published:

Source:

---

Narrated by TYPE III AUDIO.

---

Images from the article:

Apple Podcasts and Spotify do not show images in the episode description. Try Pocket Casts, or another podcast app.