Post #1846823
2026-04-26 16:52 UTC
@carloangiuli @totbwf Today my main objection, by the way, to studying these things with type theory is that those terms really refer to in-place algorithms, period. I feel the "FP" version is too radical, and relies on theorems that are too difficult, in order to make any kind of connection to the in-place algorithms that make up the canon.
Replies (1)
-
@pamorim@mathstodon.xyz 2026-04-26 18:04
@jonmsterling What's the issue with doing this style of reasoning inside a topos that has access to a local state monad? @carloangiuli @totbwf