3 ms·
Equational reasoning extends to mutation as long as you track the monad. It also smoothly devolves into Hoare Logic. It's the same tool, just applied in either
by tel 11y ago
Equational reasoning extends to mutation as long as you track the monad. It also smoothly devolves into Hoare Logic. It's the same tool, just applied in either different (monadic) contexts.
Mutation is not disallowed in PFP, by the way! You can write a perfectly great Timsort that's pure. You just can't pretend that your mutation effects are not observable when they are. (And you can use monads as type cues when that occurs).
- catnaroek 11y agoIn all fairness, Hoare logic just happens to be something I want to avoid doing as much as I can. Also, you can have a pure Timsort with linearly or affinely typed arrays. Only action-at-a-distance truly requires some framework (monads, algebraic effects, whatever) for embedding an effectul language.
- tel 11y agoYup, that's another way to do it so long as you're interested in paying the explicitness tax to introduce substructural types. My point about Hoare logic is not to promote it but instead to note that it's not categorically different from equational reasoning except in that it operates over more complex languages. And then that exactly is your tradeoff.
- pron 11y ago> You can write a perfectly great Timsort that's pure. I would be interested to learn how (with the same space complexity?), but anyway my point is that writing a provably correct Timsort using CH is harder than simply proving the imperative algorithm with a model checker.
- tel 11y agoHave a pure model of memory which is implemented directly. Associate this with a proof that the extensional side of it is pure (copying mechanics of substructural types) and you're done.
- pron 11y agoRight, but proving correctness would still be much harder than with the model checker, I think.