My first experience with formal methods

matt_d | 96 points

I think this is a very typical first response to formal methods. But eventually it becomes clear that ultimately it's not really solving any problem, but simply kicking the can to another problem. And in my opinion it's a step backwards as the can you're kicking it to is arguably more complex than where you came from.

Depending on the system you're using formal methods will rely on some set of preconditions (state before a function), postconditions (state after a function), and general state. There's nothing magical about formal methods that prevents errors, either logical/technical or by omission, here. And suddenly very small changes in program flow/logic can result in enormous amounts of work.

They're really fun and interesting, and also help you look at your code in a different way even when not using them. I think everybody has this sort of 'epiphany' moment the first time they actually play with them. But they don't work out in practice anywhere near as well as they do in theory or very limited scale. Something you quickly realize as the effort involved increases exponentially against linear increases in program size/complexity.

indubitable | 6 years ago

Formal methods are particularly effective for verifying hardware, because a) the state space is much smaller than for software (although it can still be prohibitively large for complex designs and brute force formal methods) b) people are actually ready to shell out some decent money for getting the verification done.

auggierose | 6 years ago