I wish I could give this a half-upvote.

I liked the general theme and the information here. In addition, I liked the author’s writing style. I agree with the points as far as they went. For whatever reason, however, it just didn’t connect with me on an emotional level. Perhaps the context the author used (Typescript/JS) didn’t match pain points I’m currently experiencing.

I’d also like to see the “types as axioms” idea pushed farther. I think I’m already there with Incremental Strong Typing, but I’m curious to see if others end up in the same space.

So if you’re the author, keep up the good work! I like where you’re headed

The post seems to tiptoe around the Curry–Howard correspondence. Wikipedia is quite formal, so this quote by Simon Payton Jones describes it easier:

The whole idea of Lambda Calculus really grew out of logic, and there’s very beautiful dualities between programming on the one hand, and logic on the other. It’s called the Curry-Howard Isomorphism, in which you can view a, let’s say I have a function whose type is… it takes 2 integers and it produces an integer. Well, that type tells you something about the program. So, in a sense, it’s a weak theorem about the program. It tells you something about the program, but not everything. And indeed, you could regard the program as a proof of that theorem. So, the idea of “types as theorems” and “programs as proofs” is a very deep connection between logic, on the one hand, and programming, on the other.

I’m not sure the solution to the initial motivating example is a change in mindset.

Surely you just need a type checker supporting dependant types!