[taeric]

What I meant in our industry being nothing but metaphor is basically me staring at so many OO taxonomies. Even if you ignore deep OO trees (and I think you should), it is hard not to see the way we define most data and simulations as anything other than a very formal metaphor.

That said, I was not trying to say that abstractions and types are directly metaphor. I agree with your points. My argument there was that, like metaphors, types/abstractions are never perfect.

I use types to avoid type errors. Which is a big class of error, to be sure. But they do little to help with logic errors, in my experience. And they are flat detrimental if they require pulling in more and more formalism to cover cases that are of increasingly limited ROI.

If anything, I think our industry would do well to embrace many of the modelling domains that allow use of SAT solvers to find answers. And I don't think I've ever seen a strongly typed one of those that wasn't hard to follow. (I am interested in counter examples.)