Local Reasoning for Global Properties | Hacker News Reader

Local Reasoning for Global Properties

tratt.net

36 pointsmpweiher6 comments

There's a Joel On Software post [1] in the same vein as this, which totally changed the way I think about writing software. You should aim to write software which can be verified locally with the smallest window of context. It's informed a lot of my decisions around linters, static analyzers, assertions, etc. I'm always looking for assertions that narrow state and reduce the number of lines you need to read to verify the correctness.

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/

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 checking is the same as proof verification. It is called the Curry-Howard correspondence

> 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".

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

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.

Reply on news.ycombinator.com