4 ms·
That's not entirely true. Synthesis is a popular topic within the "formal verification" umbrella. I agree that proving the software satisfies some safety prop
by kyboren 6y ago
That's not entirely true. Synthesis is a popular topic within the "formal verification" umbrella.
I agree that proving the software satisfies some safety properties and is always consistent with some specification doesn't mean that a system is truly "hacker proof".
However:
1. It's a step in the right direction, and something like a necessary condition but not a sufficient condition.
2. It's an attractive, succinct way to describe the value of formal methods and their potential (as the cited DeepSpec project intends to realize) to indeed make a truly hacker-proof system.
- ncmncm 6y agoIt's an attractive, succinct way to mislead people about the value of formal methods and their potential. Synthesis from specifications completely fails to address omissions and errors in the specifications, except insofar as they get translated to something that is more evidently wrong, or are revealed to be inconsistent.