Formal methods aren't "testing".
As you say, though, exhaustive testing is sometimes possible.
As you say, though, exhaustive testing is sometimes possible.
The work done by a a theorem prover and a fuzzer isn't all that different (and sufficiently advanced fuzzers use SMT solvers etc.)
Also, how is even "smart fuzzing" similar to theorem provers in any way? Fuzzers still think in terms of runs, but a theorem considers all cases. The best fuzzer wouldn't be able to tell if a sort algorithm works for all inputs, presuming the input size is unbounded. Actually, my understanding is that a fuzzer wouldn't be able to prove if identity function works for all kinds of objects it may be given.
The whole program? Yes.
For testing individual components, there's no need to assume. The answer is very likely either clearly yes (the input is a handful of booleans) or clearly no (the input is several integers or even unbounded) and for those cases where it's not immediately clear (one i16? Three u8s?) it's probably still not hard to think through for your particular case in your particular context.
[1] https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
Whether 4B is doable depends on how much work you're doing for each of those states, but yes, "4B" alone certainly doesn't rule it out. There's also a question of whether it goes with your most frequently run tests or is something that's only run occasionally.
> However a lot of algorithms can have more than 32 bits of states and so quickly get beyond what is doable.
I'm pretty confident we're all in agreement there.