Swimming out past intuition26 Jul 2020 ⇐ Notes archive
(This is an entry in my technical notebook. There will likely be typos, mistakes, or wider logical leaps — the intent here is to “let others look over my shoulder while I figure things out.”)
So far I’ve got
.flatMap (or alternatively,
join paired with the dynamic member subscript).
Type checking drove the implementations since I don’t grok them yet. What does it mean to
Bindings? Is that something we’d even want to do?
The compiler signaled the “reachability” of these functions, even if my understanding wasn’t there. And this is why proof assistants like Lean and community efforts behind them (the Xena project) excite me. If mathematics can be formalized to a point where assistants can guide our work in the same way a compiler does for engineering, we can swim past our present intuitions.
It’ll take a while for our collective knowledge to catch up to a lengthened line of sight, but we also needed telescopes before we could physically explore space.