> You may as well have said "then you use a magical tool that doesn't exist".
Ok, so what this tells me is that you're not aware of what modern verification techniques look like.
There's not really any one resource I can point you to, but take a look at these links. I've used these or similar technologies personally, but there are others I haven't used.
> What is your reason to think this is 'obviously' the case?
Because I've done this, and anyone who claims to be familiar with formal methods should be at least passingly familiar with all the things I mentioned.
Even if you aren't, if you've ever heard of SAT (a fairly universal CS concept) you should at least be familiar with the idea that non-exhaustive proofs are a thing.
Ok, so what this tells me is that you're not aware of what
modern verification techniques look like.
Well, techniques are not tools. I am asserting that it is quite probable that no practically useful tool exists to non-exhaustively verify the state space laydn wants to cover.
Notwithstanding your example that it's possible to non-exhaustively verify some functions on strings. There is a quite some distance between that to verifying just any function.
Because I've done this,
Sure, but how does that make it obvious to laydn that his state space is coverable? And what makes it so obvious to you that his state space is coverable? After all, the 'largeness' can have different sources, including those that make non-exhaustive methods infeasible.
I think this may be an example of the disconnect between research and the industry. Researchers say things are solved when they have shown something is possible and published about it. They feel it's then up to the industry to extrapolate, while research moves on to exciting new and greener pastures. Meanwhile the industry thinks the results are too meager, thinks the extrapolation involves a lot of technical difficulties and generally is not willing to spend enough money on what they cannot see as anything but a longshot.
If you do any model checking at all, with tools like SPIN or TLA+, you are already in the state-of-the-art minority in industry.
