3 ms·
In 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 t
by catnaroek 11y ago
In 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.