Hacker News Reader

Comment by ubertaco | Hacker News Reader

The title is not a very good one, because it's nearly a rhetorical question: no language I've ever seen -- not even Haskell -- has a type system that completely removes the need for tests. For example, even Haskell has partial functions over types like Int whose behavior can't necessarily be encoded in the type system (at least, not ergonomically/practically) and thus require actual tests to cover.

That said, I think a more accurate title for this post (based on the paragraphs beyond the first one) might be "are tests necessary for a view layer that doesn't have much business logic in it beyond passing properties when that view layer is written in Typescript?" At that point, it's really just a permutation of the question "are tests necessary for the view layer of an application?", which has highly-situational answers.

View on HN

The title is a good one, because everyone has to learn this lesson sometime. How will they learn? Well, they will probably type "Are tests necessary in typescript?" and come across this post, which will explain it to them.

Nobody is typing "are tests necessary for a view layer that doesn't have much business logic in it beyond passing properties when that view layer is written in Typescript?" into Google.

>completely removing the need for tests

That would be formal verification.

Not really. You still need tests to check whether your application is actually achieving its targets in real-world usage, including feature completeness, usability, performance; and how all of these are impacted by the environment (e.g. network issues in a distributed application).

Formal verification only tells you that the application matches its spec, given a set of assumptions. Only testing can tell you whether the spec matches the business case, and whether the spec assumptions hold.

Paraphrasing Knuth, code that has only been proven correct but not actually tested should always be approached with caution.

Edit: Knuth, not Dijkstra

Theoretically, formal verification can only tell you as much as can be encoded in a formal spec@.The problem is that no such kind of specs are known to exist (yet, if ever). As a thought experiment, if the informal specs written in English/Chinese or trapped in our head were as incomplete as a formal spec, we wouldn’t even be able to reason about what to test in the first place.

@ Then there is the limitation of verification tech of course.

Which from what I’ve seen is way harder and way less accessible than testing.

And one of the things I say to anxious coworkers who are struggling with testing is that it’s a lot harder than you think.

When I was working with CompCert, I had no problems producing a formally verified compiler that miscompiled its (meager) test suite. Tests are necessary for "formally verified" systems! You might mess up parts of the specs or the model you are verifying against. You can only catch these problems through testing.

Reply on news.ycombinator.com