Local Reasoning for Global Properties
19 points by ltratt
19 points by ltratt
I love this topic. It's not surprising that global properties can be verified from local properties: this is the principle of induction! But the key to induction is that there has to be some way to relate the local to the global, and that is what is so often lost with existing programming languages.
I'm most bullish on effect systems as the feature that drastically improves local reasoning for everyone, and I've also always been extremely interested in tierless languages that describe an entire distributed system as one program.
Have you heard about/used https://www.unison-lang.org/? I dont see it talked about much but its got the effect system and description of the whole distributed system down I think. I also love the idea of a database of ast rather than text files but I know thats a bridge too far for a lot of folks lol
It makes me think of how Bertrand Meyer's design by contract is so under used (and sadly often unknown to many an engineer). Rust Sync/Send traits are similar in principle to invariants, global properties/constraints that guarantee consistency across a code base. AI codegen seems to favour unit tests, while I would say that assertions (pre/post & invariants) are more compact and useful to maintain consistent behaviour, and then swapping unit for integration tests, to move the focus from local behaviour to global, ideally end-to-end behaviour.