Post #1782105
2026-04-23 01:13 UTC
@mdhughes While on very many painkillers, everything came to make sense to me. Before procedural abstraction, they develop the gist of their modules as
requires assertion
BODY
effects assertion (+ modifies assertion)
on the hypothesis that a user of a module is expected to ignore the implementation details of bodies for given requires/effects assertions.
In my conditions shindig, I am developing instead
conditions - LHS handler bodies
restarts - RHS bodies
But insisting bodies be in ACL2 FOL
Replies (1)
-
@screwlisp@gamerplus.org 2026-04-23 01:16
@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,