As <cat-over-keyboard> already mentioned, it's not always that simple. For example, my current approach (modeled after Krom, who doesn't even have a Wikipedia page - no wonder nobody reads him!) is a more systematic search for a polynomial algorithm - construct a polynomial sized-logic in which theories have models that are satisfying instances of SAT, and prove its refutable-completeness. This proves existence of a polynomial algorithm, because you can generate all formulas of theory (coming from SAT instance) in said logic, and if you don't find a contradiction, the instance is satisfiable. The algorithm is kinda implicit, non-deterministic, if you will (because you can generate all the formulas in any order or even generate just a subset).

Anyway, my main point is - people beware, practically solvable P=NP (even for hard instances) is a very real possibility.

Sure, but most complicated polynomial time algorithms don't work like this. You either have cases like AKS which are obviously polynomial but not obviously correct, or cases that are obviously correct but not obviously polynomial.