The 4 horsemen of unsoundness in OO languages
summary
Four concrete pitfalls: a pair of independently verified implementations that call each other via an interface produce nontermination despite each being marked total (demonstrating modular termination impossible for a binary total/non-total discipline); using a ghost field holding a lambda (Omega) encodes divergence to force false and break Dafny‑style systems (ghost + partial correctness → unsound); contracts that refer to each other are ill‑founded and provably inconsistent; encoding observations via added primitives wrecks subtyping and realism.
AI-written summary · about
chapters (4)
- 0:00Start
- 3:48The current narrative
- 9:283 companies working independently
- 17:52Ghost + partial correctness = unsound
related talks
22mFrom FP to OOP and Back, Consistently
01h 02mBasics Designs and How We Got Them Wrong
01h 02mLanguage Design meets Verifying Compilers
01h 32mPlenary: Six Impossible Things
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
32mThe Evolution of Object-Oriented Programming
31mTermination in Concurrency, Revisited
26mInfinite Possibilities