I have to admit I went in very pessimistic about the high-level pitch of this piece, but I’m more convinced than before. The extra assertion at the call site in particular is an interesting concept because it renders explicit what sort of contract we are relying on at that specific call site, which can be important for refactoring. [0]
I do think that people, in their hearts, wish that static assertion verification were easier in mainstream languages. ADTs are often cited as a way of doing this, but the fact that you can’t do variant narrowing in most languages at the type level greatly reduces their utility on this front. I find myself wanting Typescript’s type narrowing capabilities everywhere.
TS-style type narrowing won’t solve the point about distributed systems having different truths, of course. But for some of the simpler stuff mentioned… if it’s important enough to have asserts, and if it is easy to create data types to track invariants, then we could get static checks on this really easily.
[0]: An aside, but this is why I think long and pedantic function names are helpful in many cases. addToEnd instead of push, requeryFromDatabase vs refresh, saveIfDirtyBitEnabled vs save…. If it’s everything it’s pretty miserable but for messy business logic it’s a lifesaver for forcing people to declare intent.
I do think that people, in their hearts, wish that static assertion verification were easier in mainstream languages
Yup, I think you nailed it! I want to write code that is provably correct, but I don’t want the proof parts to obscure the actual logic implemented by the code. Not only we need a proof, the proof also needs to be easy and lightweight.
Zig and Rust make for an interesting contrast here. Suppose you have a function, and it really wants to have some ad-hoc return type just for this function. In Rust, that’s a high overhead wish: you could define enum FooResult, but then your callers need to import this enum to use your function, the enum might have to be declared far away from the function itself (if it is in an impl block), and just typing FooResult::Bar gets tiresome. In contrast, in Zig you’d just
fn foo() union(enum) { bar: u32, baz } {
…
}
and off you go. On the one hand, this is, on the surface, mostly syntax, which doesn’t matter. On the other hand, this dramatically reduces the costs of using more precise types.
The function postcondition might actually be stronger than what is required at the call site, so assertion after-the-call could be a different, weaker one.
IIUC, this is like the consequence rule from Hoare logic.
The function postcondition should/could assert the maximally-restrictive condition it can, while call site postconditions can assert any weaker consequence of the function’s postcondition. (E.g., a square() fn might assert some mathematical property of squared numbers, but maybe a call site only cares that the return value is positive.)
I have to admit I went in very pessimistic about the high-level pitch of this piece, but I’m more convinced than before. The extra assertion at the call site in particular is an interesting concept because it renders explicit what sort of contract we are relying on at that specific call site, which can be important for refactoring. [0]
I do think that people, in their hearts, wish that static assertion verification were easier in mainstream languages. ADTs are often cited as a way of doing this, but the fact that you can’t do variant narrowing in most languages at the type level greatly reduces their utility on this front. I find myself wanting Typescript’s type narrowing capabilities everywhere.
TS-style type narrowing won’t solve the point about distributed systems having different truths, of course. But for some of the simpler stuff mentioned… if it’s important enough to have asserts, and if it is easy to create data types to track invariants, then we could get static checks on this really easily.
[0]: An aside, but this is why I think long and pedantic function names are helpful in many cases.
addToEndinstead ofpush,requeryFromDatabasevsrefresh,saveIfDirtyBitEnabledvssave…. If it’s everything it’s pretty miserable but for messy business logic it’s a lifesaver for forcing people to declare intent.Yup, I think you nailed it! I want to write code that is provably correct, but I don’t want the proof parts to obscure the actual logic implemented by the code. Not only we need a proof, the proof also needs to be easy and lightweight.
Zig and Rust make for an interesting contrast here. Suppose you have a function, and it really wants to have some ad-hoc return type just for this function. In Rust, that’s a high overhead wish: you could define
enum FooResult, but then your callers need to import this enum to use your function, the enum might have to be declared far away from the function itself (if it is in an impl block), and just typingFooResult::Bargets tiresome. In contrast, in Zig you’d justand off you go. On the one hand, this is, on the surface, mostly syntax, which doesn’t matter. On the other hand, this dramatically reduces the costs of using more precise types.
IIUC, this is like the consequence rule from Hoare logic.
The function postcondition should/could assert the maximally-restrictive condition it can, while call site postconditions can assert any weaker consequence of the function’s postcondition. (E.g., a square() fn might assert some mathematical property of squared numbers, but maybe a call site only cares that the return value is positive.)