I was with you until: > 5) Too much gratuitous abstraction. The old version was "everything is predicate calculus". The new version is "everything is a type" a

I was with you until: > 5) Too much gratuitous abstraction. The old version was "everything is predicate calculus". The new version is "everything is a type" and "everything is functional". Total functional programming with types is literally the same as writing proofs in intuitionistic logic, in a technical sense (the Curry Howard correspondence). This isn't a new fad. It's a deep result that was known more than half a century ago.