This is an important point: even a finite search space quickly gets out of hand in practical terms. I've worked a bit on bounded verification which comes down to comparing loop-free programs with finite inputs for equality. It is not easy in practice! Modern approaches use sophisticated proof search algorithms (ie SMT solvers) and still struggle to scale beyond relatively small and simple programs. I don't know the numbers off-hand because verification was not the bottleneck in my application, but I suspect that even sophisticated modern methods scale poorly beyond a few hundred instructions or for large inputs (ie algorithms with complex behavior over arrays).

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.