What do we mean by "unsound"?
summary
Defines unsound model as one that validates a formula but fails when interpreted into the real system, giving concrete examples: reference-semantics models break on C pointer aliasing; models that assume termination miss nonterminating behavior. Shows unsound interpretation where equalities disappear under translation, and cites how combining UIP and univalence axioms makes a prover inconsistent. Points to tool bugs that let one prove false, Java’s broken subject-reduction causing ClassCast at runtime, and practical risks from ignored stack limits and deployment/CI mismatches.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:32General picture
- 2:44Logic
- 5:43Interpretation
- 6:58Equalities
- 9:11Unsound Models
- 12:52Sound Models
- 24:05Is unsound a bug
- 27:16Failure of subject reduction
- 29:35Unsoundness in resources and hardware
- 36:31Reality check
- 38:21Why I care
related talks
14mModeling Reachability Types with Logical Relations -- Semantic Type Soundness,(…)
20mOn Extending Incorrectness Logic with Backwards Reasoning
27mUnrealizability Logic
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
18mSemantic-Type-Guided Bug Finding
22mA Categorical Basis for Robust Program Analysis
13mRevealing Sources of (Memory) Errors via Backward Analysis
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)