On October 5, 1960, the American Ballistic Missile Early-Warning System station at Thule, Greenland, indicated a large contingent of Soviet missiles headed towards the United States. Fortunately, common sense prevailed at the informal threat-assessment conference that was immediately convened: international tensions weren't particularly high at the time. The system had only recently been installed. Kruschev was in New York, and all in all a massive Soviet attack seemed very unlikely. As a result no devastating counter-attack was launched. What was the problem? The moon had risen, and was reflecting radar signals back to earth. Needless to say, this lunar reflection hadn't been predicted by the system's designers.

Over the last ten years, the Defense Department has spent many millions of dollars on a new computer technology called "program verification" - a branch of computer science whose business, in its own terms, is to "prove programs correct" . [...]

What, we do well to ask, does this new technology mean? How good are we at it? For example, if the 1960 warning system had been proven correct (which it was not), could we have avoided the problem with the moon? If it were possible to prove that the programs being [...]

---

Outline:

(03:31) The Machine Learning Part

(04:52) A Technique Which Won't Work: Supervised Learning

(06:16) Latent Variables and Problem Statement

(08:02) Some Candidate Properties And Assumptions

(08:41) Assumption 1: Capability

(09:32) Mathematical Property 1: Real Pattern & Correspondence Principle

(10:50) Mathematical Property 2: Convergent Factorization

(12:42) Limitations

---

First published:
November 29th, 2025

The Limits of Correctness

Mentioned by

Mentioned in 0 episodes

The AI-powered Podcast Player