> Yes, it would help a tiny little bit if the compiler would check for nullable pointers. But this comes at a cost of annotation work / maintenance work / worse modularity, and it only helps a bit. There are so many more invariants (is this integer in the range 3-42 and odd or divisible by 12, is that integer a valid index into this other dynamic array...) that you can't practically check with a static system, and they are much much worse because many of them manifest themselves in much subtler ways.
Not my experience. It's no more work since you know when you're writing whether it's nullable, it's better for maintenance since you can immediately see which variables are nullable. As for other invariants: look at how often you see a real app you're using fail, or look at the bugs that manifest in production; they're rarely the subtle ones, most of them are the simple stupid cases.
> All these formalisms work in some toy examples, but adhering to them makes a big mess as soon as it gets a little more complicated. Most basic example, const.
No, const is a poor example; it's a wrong abstraction and it's difficult to use as a result.
Not my experience. It's no more work since you know when you're writing whether it's nullable, it's better for maintenance since you can immediately see which variables are nullable. As for other invariants: look at how often you see a real app you're using fail, or look at the bugs that manifest in production; they're rarely the subtle ones, most of them are the simple stupid cases.
> All these formalisms work in some toy examples, but adhering to them makes a big mess as soon as it gets a little more complicated. Most basic example, const.
No, const is a poor example; it's a wrong abstraction and it's difficult to use as a result.