New Bob Nystrom blog post! Always going to upvote that.
More substantially, I was thinking of Typescript's control flow analysis as soon as I started reading through the "Record cases" section, I was already thinking of commenting on it, and then the next section anticipated my thoughts. I can definitely understand that being difficult to implement in the general case, but I'm curious if it'd be workable within the context of a single statement/expression. I'm envisioning something like Go's .(type) syntax. You'd probably need to restrict what would be allowed within each case branch, though, and that could get tricky and unintuitive to use.
His solution and syntax remind me of Ada's variant records. Despite Ada's focus on safety, it also resorts to runtime exceptions for incompatible fields in that case. That's probably a local maximum in the language design space.
Ada offers formal verification to remove checks, they can also be removed without formal verification but that is not a sane thing to do.
Ada feels like it is more about writing the correct intent of programmers and caring more about intent than any other thing. For example, the pre and postconditions are not always meant to be 100% verifiable, its fine for them to not be verifiable, the checks are more important than the verifiablility of them.
More substantially, I was thinking of Typescript's control flow analysis as soon as I started reading through the "Record cases" section, I was already thinking of commenting on it, and then the next section anticipated my thoughts. I can definitely understand that being difficult to implement in the general case, but I'm curious if it'd be workable within the context of a single statement/expression. I'm envisioning something like Go's .(type) syntax. You'd probably need to restrict what would be allowed within each case branch, though, and that could get tricky and unintuitive to use.