Hacker News Reader

Comment by User23 | Hacker News Reader

Interesting. Incidentally, I would claim that TDD done properly is in fact a lightweight formal method. It helps to be conversant with some kind of formal semantics, but you can definitely play a bit fast and loose by treating your tests as a lightweight specification. In that case any formal properties I want the code to have that can't practically be expressed in the test is included in a comment on the test. Also, fuzzing is a way to narrow that gap further.

View on HN

Property-based tests let us state the formal properties we want, even though we can't verify them. For example, ScalaCheck lets me state the following:

    forAll (x: Int) { assert(x.abs >= 0) }

This is useful as a spec, as documentation, and as a test suite: e.g. ScalaCheck can try to disprove such properties by checking a bunch of random inputs.

Whilst such approaches don't let us prove such statements (except for exhaustively checking small input spaces, e.g. `forAll (x: Boolean, y: Boolean) ...` only needs four tests), I find it just as easy as normal unit testing, and far less effort than formal proofs (e.g. using Coq or Agda)

(FYI that property is in fact false, since it doesn't hold for -2147483648; ScalaCheck's random generators are biased towards such "problematic" values, e.g. -inf, NaN, etc., so it usually find such things)

A failing test can only prove the existence of a bug. A passing test can not prove that there are no bugs.

Neither can a formal spec.

That's a category error. The formal spec isn't a proof, it's what is to be proven. Without a spec the notion of programming errors has no formal meaning. In that case, the complaints about the bug are always with respect to pleasantness. Given a formal specification, it's possible to write a program that will reliably satisfy that specification. And the tooling is better than ever. The Dafny language out of Microsoft Research is one interesting example. One can also do it by hand, possibly using an SMT solver to check one's work.

Believe me, I take Dijkstra's message to heart. And a quality test suite can reify the decisions of a formal specification as expressed in PTS or some other suitable abstraction. Think more here's the proof, more or less rigorous as circumstances suggest reasonable, and here's some tests that capture as much of that in code as practicable to help give us some further confidence that we didn't err in our manipulations.

> I would claim that TDD done properly

"I get paid for code that works, not for tests, so my philosophy is to test as little as possible to reach a given level of confidence" — Kent Beck

https://stackoverflow.com/a/153565

Yes, as a consultant Mr. Beck has no concern about code correctness. He only needs it to please the client sufficiently to maintain his reputation. Since users are used to low quality software, that’s a practicable bar to meet just winging it.

And as a seller of programming books, he increases his target audience by excluding the small percentage of mathematically literate programmers and appealing to the majority who find logic intimidating.

Reply on news.ycombinator.com