> Perhaps this will be the push we need to finally, seriously consider the possibility that our formalisms of “efficient” and “efficiently verifiable” algorithms correspond to nothing resembling reality,

What do you mean? Do you mean that our heuristics shortcuts of treating P as efficiently solvable (and NP as efficiently verifiable) are not warranted? So far pretty much all algorithms in P that we found have small exponents. That hasn't changed, but it might change in the future.

Or do you mean something else?

Keep in mind that even most instances of many NP hard problems can be solved very efficiently in practice, because most instances ain't hard.

However we know problems that are expected to be 'easier' than NP that are hard to solve in practice. These are pretty much all the problems we build cryptography out of, because essentially these problems are in the intersection of NP and co-NP and that's expected to be smaller than NP. And cryptography has to be hard to break on average to work: a random key needs to be a good key.

> and P \in NP is actually ill-posed.

Oh, that's very simple to answer: P is not an element of NP. The question people care about is whether there's any element in NP that's not in P. In LaTeX notation P \subset NP vs P \subseteq NP.

I'm not sure what you mean by ill-posed? The question is very clear. What are you trying to say?