5 ms·

Source code is a poor way to specify the behavior of a system. It is complex, verbose, and difficult to reason about without proper language abstractions at app

Source code is a poor way to specify the behavior of a system. It is complex, verbose, and difficult to reason about without proper language abstractions at appropriate levels. Worse still are machine optimizations obscuring intent as the software evolves, work-around "patterns" for inferior PL designs, and other savageries inflicted upon us. It is highly unlikely you could give a brilliant programmer a few hundred thousand or millions of lines of code and ask them what the program does in an afternoon let alone ask them to find the bug in it. Good unit tests provide the specification for a certain low-level of the code to a developer. You will never catch everything but their purpose is not to test for absolute correctness. Their purpose is to specify, for a given range of expected behavior, what the boundaries are. If I write the test first in earnest I am telling my future maintainers what I intended to write. We can execute that intention against what I wrote and make assertions about whether it works as expected. That's all I expect unit tests to do. Formal correctness proofs for all possible inputs is way out of my league and beyond the scope of almost every project I've encountered save for automated proof verification software. You should write unit tests and you should write them first. They are the executable specification you will run your program against to ensure your software behaves in the manner in which you intended it to. With solid, well-thought out tests guiding your design you should be able to optimize and refactor your software over time and see that it still behaves as expected in the face of change. And you should be able to hand a suite of well-written tests to a new developer and expect them to understand what a given piece of software does in a day (perhaps in even less time for smaller pieces).

radicalbyte 13y ago
Spot on. Unit Tests aren't there to ensure that you get the right answer. It's there to ensure that you've asked the right question. Or at the very least to document the thought process of the person implementing code. Use static analysis tools + code reviews to improve correctness, and unit tests to guide design + document.
- googletron 13y ago
  Unit tests aren't for asking the right question. There code is there and readable (hopefully) so that shouldn't be an issue. Unit tests are there to ensure when you need to make a change you don't include a regression (moving code backwards). Missed something that the function was previously doing. They aren't useless and have a clear place in testing. Unit tests alone can't guarantee a fully tested system, but they minimize engineer error when working on various pieces of a code base, but this is predicated on cleanly separated and testable code pieces.
  - FeloniousHam 13y ago
    Can't you both be right? Another facet: unit tests are the living, useful documentation of the code. Starting on a team with a large legacy code base, unit tests are the tutorial on the best practices of the API. This magnified if the "unit" tests include full functional test with an embeddable container (eg. OpenEJB). (apologies for parroting the gp)
  - tormeh 13y ago
    Code is never readable. The "self-documenting code" mantra can only be applied to edge cases and toy problems. This is simply because the human brain is really bad at reading code. The level of abstraction optimal for human consumption is so high that reading precise instructions is a pain.
tel 13y ago
I agree with everything you've said except the line about formal correctness proofs. I'd in fact be willing to replace "unit tests" with correctness proofs at almost every point in your comment and stand behind it myself... given that I get to define "correctness proof" carefully. In particular, I want to appeal for using "the most formal thing reasonable" whenever possible. If you're writing highly abstract code, you would likely be amazed at how simply you can write down and prove it's behavior. For less abstract code, some formal properties may still be available and provable, some available but difficult to prove and better verified using exhaustivity or probabilistic property checking [0], and finally some are simply unknown. My point is that unit tests are one of the very weakest forms of verification. They should be traded for more powerful techniques at every availability. Availability is, today, still an issue, but this is precisely why dependently typed language research is interesting. In Idris you can write your core code alongside a machine-checked proof of its correctness. You can verify your outside interface by nearly autogenerating an interface fuzzer and checking encode/decode roundtrips or system fixed points. Finally, you can compile the whole thing down to Javascript and deploy it atop Meteor if that's your endgame. Idris is just one interesting point on this spectrum. I think availability of formal correctness proving (in capability, expression, organization, and automatic execution) will be a major force in the future of CS. [0] http://en.wikipedia.org/wiki/QuickCheck http://en.wikipedia.org/wiki/QuickCheck
- agentultra 13y ago
  Maybe it's because lisp has warped my brain but I'm not entirely sold on dependent type systems and formal proofs yet. It will be interesting to see if there's anything worthwhile that falls out of it as a consequence of such research but I don't think it's very interesting in its current state. It could use more exploration and I look forward to seeing what comes of it.
  - tel 13y ago
    Heh, I find it the next step in evolution after lisp. All the same flexibility, but with a new language that lets you delineate and work with the meaning of your data alongside the data itself. I don't think it's anything resembling practical in its current state, but I think it's absolutely the way of the (possibly deep) future. I want to spend more of my time programming with types than programming with values since that's where my brain honestly is (despite the type languages of today being a bit obtuse) and since the compiler is often able to program the value-level stuff for you.

radicalbyte 13y ago

Spot on. Unit Tests aren't there to ensure that you get the right answer. It's there to ensure that you've asked the right question. Or at the very least to document the thought process of the person implementing code. Use static analysis tools + code reviews to improve correctness, and unit tests to guide design + document.

googletron 13y ago
Unit tests aren't for asking the right question. There code is there and readable (hopefully) so that shouldn't be an issue. Unit tests are there to ensure when you need to make a change you don't include a regression (moving code backwards). Missed something that the function was previously doing. They aren't useless and have a clear place in testing. Unit tests alone can't guarantee a fully tested system, but they minimize engineer error when working on various pieces of a code base, but this is predicated on cleanly separated and testable code pieces.
- FeloniousHam 13y ago
  Can't you both be right? Another facet: unit tests are the living, useful documentation of the code. Starting on a team with a large legacy code base, unit tests are the tutorial on the best practices of the API. This magnified if the "unit" tests include full functional test with an embeddable container (eg. OpenEJB). (apologies for parroting the gp)
- tormeh 13y ago
  Code is never readable. The "self-documenting code" mantra can only be applied to edge cases and toy problems. This is simply because the human brain is really bad at reading code. The level of abstraction optimal for human consumption is so high that reading precise instructions is a pain.

tel 13y ago

I agree with everything you've said except the line about formal correctness proofs. I'd in fact be willing to replace "unit tests" with correctness proofs at almost every point in your comment and stand behind it myself... given that I get to define "correctness proof" carefully. In particular, I want to appeal for using "the most formal thing reasonable" whenever possible. If you're writing highly abstract code, you would likely be amazed at how simply you can write down and prove it's behavior. For less abstract code, some formal properties may still be available and provable, some available but difficult to prove and better verified using exhaustivity or probabilistic property checking [0], and finally some are simply unknown. My point is that unit tests are one of the very weakest forms of verification. They should be traded for more powerful techniques at every availability. Availability is, today, still an issue, but this is precisely why dependently typed language research is interesting. In Idris you can write your core code alongside a machine-checked proof of its correctness. You can verify your outside interface by nearly autogenerating an interface fuzzer and checking encode/decode roundtrips or system fixed points. Finally, you can compile the whole thing down to Javascript and deploy it atop Meteor if that's your endgame. Idris is just one interesting point on this spectrum. I think availability of formal correctness proving (in capability, expression, organization, and automatic execution) will be a major force in the future of CS. [0] http://en.wikipedia.org/wiki/QuickCheck http://en.wikipedia.org/wiki/QuickCheck

agentultra 13y ago
Maybe it's because lisp has warped my brain but I'm not entirely sold on dependent type systems and formal proofs yet. It will be interesting to see if there's anything worthwhile that falls out of it as a consequence of such research but I don't think it's very interesting in its current state. It could use more exploration and I look forward to seeing what comes of it.
- tel 13y ago
  Heh, I find it the next step in evolution after lisp. All the same flexibility, but with a new language that lets you delineate and work with the meaning of your data alongside the data itself. I don't think it's anything resembling practical in its current state, but I think it's absolutely the way of the (possibly deep) future. I want to spend more of my time programming with types than programming with values since that's where my brain honestly is (despite the type languages of today being a bit obtuse) and since the compiler is often able to program the value-level stuff for you.