Type systems are getting more interesting as time goes on as innovations from research and niche languages are making it into the mainstream. A particularly interesting one to me is dependent types. That's where you can start to prove more interesting things about your code. It's juuuust beginning to make its way into practical use. I'd expect once that happens, we might see a gradual transition towards proving more and more invariants and properties of your code.
The curry lambek howard isomorphism has been known for a while. Coq, the language that is used by the posted textbook is a dependently typed language and was released 30 years ago.
Nobody builds web servers in Coq, but they do in Haskell, which I believe has some form dependent types coming. That's the kind of moving from niche languages to increasingly mainstream ones I mean. From there, maybe eventually it gets refined and even later properly mainstream.
Sorta, but not precisely. But it's the kind of progress I see as encouraging for the future of formal methods in mainstream software development.
