Post #1782106
2026-04-23 01:16 UTC
@mdhughes
ACL2 FOL -> Applicative common lisp, first order logic.
This gives me the opposite to Liskov and Guttag's abstraction by specification, where you formally write before and after assertions for reasoning.
Instead, my "abstraction by condition" a-b-c, I associate LHS bodies with (linearized) condition names and RHS bodies with (computed, linearized) restart names, and use a fully automatic prover on the bodies. So all the bodies are formally checked, and I can reason about the names,
Replies (1)
-
@screwlisp@gamerplus.org 2026-04-23 01:17
@mdhughes Rather than having assertions about the names formally checked for reasoning about the bodies. WILL THIS STILL BE TRUE ON LESS PAINKILLERS, WHO KNOWS