On: AI will make formal verification go mainstream

[bluerooibos]

Is there a difference here between a proof and an automated test?

I'm curious what a proof would look like compared to my RSpec unit tests and what the actual implementation would look like.

[pizlonator → bluerooibos]

A test tests some - but not all - of the paths through your code. And some - but not all - of the inputs you might see.

A proof establishes that your code works correctly on all paths, inputs, etc.

[i_am_a_peasant → pizlonator]

A “proof” in the formal verification sense is just an exhaustive search through a state space that a model of your system, respects a certain set of constraints you have to explicitly write.

You could still have written the model wrong, you could still have not accounted for something important in your constraints. But at least it will give you a definite answer to “Does this model do what you say it does?”.

Then there are cases when an exhaustive search of the entire state space is not possible and best you can do is a stochastic search within it and hope that “Given a random sampling of all possible inputs, this model has respected the constraints for T amount of time, we can say with 99.99999998% certainty that the model follows the constraints”.