Is Peter Correct or Incorrect?

on YouTube ↗24m

" summary

Claims that incorrectness logic is the dual of Hoare-style total/partial correctness under abstract interpretation and gives a constructive, sound-and-complete proof system. Uses an angelic relational semantics, fixed-point transfer theorem, abstractions (post/pre/graph and negation), and the AEL correspondence to compute the theory; employs fixpoint induction (Park/Scott variants) and a fixpoint approximation for loops. Builds a proof system by turning the computed theory into rules and shows it works (no separate consequence rule needed) and that debuggers implement this under‑approximation view.

AI-written summary · about

" chapters (17)

1. 0:00Peter’s incorrectness logic
2. 1:11Logic singularities and universality
3. 2:37Fixed point semantics
4. 3:58Relational semantics for incorrectness
5. 5:29Abstraction and isomorphism
6. 7:41Strongest post vs incorrectness
7. 9:11Fixed point abstraction for loops
8. 10:18Strongest post and negation
9. 11:00Proof system design
10. 13:31Fixed point induction
11. 16:23Consequence rules
12. 17:49Rules in incorrectness logic
13. 18:35Evaluating Peter’s logic
14. 19:38Debugging as incorrectness
15. 20:24Over and under approximation
16. 22:12Duality in induction
17. 22:54Conclusion