ZARZA We are Zarza, the prestigious firm behind major projects in information technology.
Listen "Technical reasons for lack of adoption of computer-checked proofs"
Episode Synopsis
Discussion of a technical reason for lack of adoption of computer-checked proofs for mathematics, namely the level of detail in the proof. Proof assistants require too much detail in proofs to allow mathematicians to carry over their elegant art of expressing just the right amount of information to convey the idea of the proof to a mathematically competent reader. For Computer Science, a problem of adoption is that proofs are computationally useless (generally).
More episodes of the podcast Iowa Type Theory Commute
Measure Functions and Termination of STLC
14/11/2025
Schematic Affine Recursion, Oh My!
22/08/2025
The Stunner: Linear System T is Diverging!
19/08/2025
Terminating Computation First?
01/08/2025
A Measure-Based Proof of Finite Developments
16/04/2025
Nominal Isabelle/HOL
31/01/2025
The Locally Nameless Representation
02/01/2025
In God we trust