3 ms·

TDD, formal verification i'd say yes

• didibus 10y ago
  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.
  • jononor 10y ago
    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 http://www.scalatest.org/user_guide/property_based_testing
  • 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 ago
      How would we specify P? I can't get away from the idea that specifying P is similar to constructing T.
      • User23 10y ago
        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.
        • undershirt 10y ago
          This is probably difficult to explain without proper context, but could I ask you for a summary? (Thanks for the book references.)