5 ms·
Formal verification will never catch on, because it's silly and prohibitively difficult for all but the simplest programs. On the other hand, formal constructi
by User23 10y ago
Formal verification will never catch on, because it's silly and prohibitively difficult for all but the simplest programs.
On the other hand, formal construction is an idea whose time is long overdue. Rather than asking if program text T satisfies predicate P, instead start with P and then construct a T mechanically such that it must satisfy P. The latter is a much easier task than the former. Sort of like how it's easy to know N is the product of two large primes if you just multiplied two large primes together to get it.
- undershirt 10y agoHow would we specify P? I can't get away from the idea that specifying P is similar to constructing T.
- User23 10y agoDijkstra and Scholten's Predicate Calculus and Program Semantics is a good textbook on the subject. Dijkstra's a Discipline of Programming is much more informal, but I find it more readable and it has a number of good examples.
- undershirt 10y agoThis is probably difficult to explain without proper context, but could I ask you for a summary? (Thanks for the book references.)