[btilly]

The "non-constructively" in this case has fascinating consequences.

One of those is that according to classical mathematics there are concrete problems with polynomial time algorithms that there is no way of producing, and if produced, there is no way of verifying. (Literally no way of verifying, pick an axiom system and there are problems for which the question of whether there is one more forbidden minor is undecidable in said axiom system.)

If you doubt that such algorithms have any real existence, you might be a closet constructivist...