In Bill's post earlier this week, he asks if there is a fixed algorithm such that if P = NP, this algorithm will correctly compute satisfiability on all inputs. While I believe this statement is true because P ≠ NP, I would like to argue we won't prove it anytime soon. Bill links to a TCS Stack Exchange answer by Marzio De Biasi giving a fixed algorithm that would get SAT correct except on