Local Reasoning for Global Properties(tratt.net)
tratt.net
Local Reasoning for Global Properties
https://tratt.net/laurie/blog/2026/local_reasoning_for_global_properties.html
6 comments
The concept is brilliant and excellently demonstrated, but I do want to nitpick the examples a little!
Type narrowing can represent “this cannot happen” situations!
List -> NonEmptyList, for example. NonEmptyList would refuse to be constructed from an empty list & check for emptiness in its remove() method..
Same for narrowing states A, B and C down to “state A cannot happen here” ie. only B and C are possible. That’s just a new enum!
Typescript’s compiler can automatically perform narrowing.
The downside of manually narrowing is more code, but the upside is clarity. The other downside is the system ends up fussier about what it’ll accept.
What’s a thought experiment though, is the huge value of codifying enforcement mechanisms for properties we desire. This lets the computer verify those properties itself without human intervention. “Does the code compile?” on steroids. There’s tremendous leverage in giving the nondeterministic part of the computer tools to verify things deterministically, and letting it use them itself.
Type narrowing can represent “this cannot happen” situations!
List -> NonEmptyList, for example. NonEmptyList would refuse to be constructed from an empty list & check for emptiness in its remove() method..
Same for narrowing states A, B and C down to “state A cannot happen here” ie. only B and C are possible. That’s just a new enum!
Typescript’s compiler can automatically perform narrowing.
The downside of manually narrowing is more code, but the upside is clarity. The other downside is the system ends up fussier about what it’ll accept.
What’s a thought experiment though, is the huge value of codifying enforcement mechanisms for properties we desire. This lets the computer verify those properties itself without human intervention. “Does the code compile?” on steroids. There’s tremendous leverage in giving the nondeterministic part of the computer tools to verify things deterministically, and letting it use them itself.
> The downside of manually narrowing is more code, but the upside is clarity.
This, IMHO, is where things get tricky: quite often, writing more code is at odds with clarity. I don't think there's a simple relation here -- more sometimes is better! -- and for me at least I don't know how to define it any better than "I know it when I see it".
This, IMHO, is where things get tricky: quite often, writing more code is at odds with clarity. I don't think there's a simple relation here -- more sometimes is better! -- and for me at least I don't know how to define it any better than "I know it when I see it".
Type checking is the same as proof verification. It is called the Curry-Howard correspondence
Interesting. In the Rust world extensions like Verus, I think, are trying to enable exactly what the author is discussing. Perhaps worth a look:
https://github.com/verus-lang/verus
https://github.com/verus-lang/verus
Defensive checks are good and it's the compiler's job to optimize them away.
A simple comment can tell future readers that it's not actually expected to be possible.
A simple comment can tell future readers that it's not actually expected to be possible.
Rust has definitely caught my eyes a few times here, since most of what I described is manual. Particularly in the embedded space RTIC [2] has some really neat stuff going on. Other languages have good type systems and spatial memory safety, but nothing else seems to have Rust's killer features around concurrency.
[1] https://www.joelonsoftware.com/2005/05/11/making-wrong-code-...
[2] https://rtic.rs/2/book/en/