Hacker News Reader

Comment by xj9 | Hacker News Reader

TDD, formal verification

i'd say yes

I know TDD has gotten out of fashion, where people seem to acknowledge today that the right balance of tests is better, more practical, then a test first and test everything approach.

Formal verification hasn't really caught on yet. The extra effort needed to formally prove even a trivial program seems to be too high for the value it gives to most stakeholders.

I'm really hopeful for simpler methods of formalized proofs, or even automated testing. I think today, the practical cost is maybe still too high for people to care.

Property-based testing can sometimes be a practical step inbetween unit-testing and formal proofs. Scala is where this is most common/well-supported, I think http://www.scalatest.org/user_guide/property_based_testing

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.

How would we specify P? I can't get away from the idea that specifying P is similar to constructing T.

Dijkstra 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.

This is probably difficult to explain without proper context, but could I ask you for a summary? (Thanks for the book references.)

Reply on news.ycombinator.com