A similar method is used in matrices to compute AB =? C in O(n^2) time (you check a predefined number of rows). You get O(n^2.something) if you do the actual multiplication
f1(x) = (x==7239829489) ? 0 : x
f2(x) = x
As the wiki article states, "Currently, there is no known sub-exponential time algorithm that can solve this problem deterministically. However, there are randomized polynomial algorithms for testing polynomial identities."
[1]https://en.wikipedia.org/wiki/Schwartz–Zippel_lemma
(Note that this is in the context specifically of polynomial function equivalence.)
That's fine if you just need a high enough confidence for military encryption or financial transactions. But what if you're trying to prove a theorem about them, and just can't take any chances?
[1] Believe it was in Aaronson's Quantum Computing Since Democritus
On the one end are "point tests", manually written tests that check correctness in several predetermined cases. That's what most software engineers mean by "testing".
Then comes randomized tests/fuzz testing/QuickCheck where properties are defined to hold for all values of some variables and then can be checked on randomly generated values. This offers better correctness guarantees than manually created "point tests" but might still miss failing cases since it's sampling and not exhaustively searching through the whole space.
Finally, on the far end are proofs, where one formally proves that the formerly mentioned properties always hold. I cannot imagine a stronger guarantee that something holds than an actual mathematical proof of it.
Dependently typed languages (Agda, Idris, Coq, Lean, etc) push software development into that far end where correctness can actually be proved. Imo that's where the future of software lays for certain classes of programs where correctness is a must.
Here's a proof of the original question in Lean:
def foo : (λ x, 2 * x) = (λ x, x + x) :=
begin
apply funext, intro x,
cases x,
{ refl },
{ simp at *,
dsimp [has_mul.mul, nat.mul],
have zz : Π a : nat, 0 + a = a := by simp at *,
rw zz }
endfor any input space in which a finite number of checks has greater than literally 0% (measure zero) of being representative this problem is trivial (finite space).
If you have a function that takes a single 32-bit floating point input and runs in, say, 100 cycles, you can test all the possible inputs in a couple minutes or so. If you have multiple floats as inputs or the function is more complex, you can exhaustively check it with an SMT solver or the like. If your function depends on hundreds or thousands of inputs and has complex looping logic, you probably can't exhaustively check it with any automated solution.
Real programs, of course, are orders of magnitude more complex than even the last example. Verifying them automatically is effectively impossible even if they have finite inputs, guaranteed bounds on loops and are "trivial" in the mathematical sense.