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).
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.
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.
The way I see formal correctness proofs is that they'll be useful, but not a panacea.
If I have a method that takes a List as a parameter, and returns an Integer, then congratulations - I have just written a formal proof that it is possible to derive an Integer from a List.
However, the business need wasn't to derive an Integer from a List - it was something far more specific.
So that's why people like the idea of dependent types, in that you can make the type system (mostly) Turing complete, and actually make the types reflect the specification of the problem.
And then if you write an implementation of that specification, congratulations, you have proved that that implementation is correct.
Which is pretty cool, except that it overlooks the fact that a very large percentage of our bugs are not in our implementation, but in our agreed-upon specification. Almost every bug I encounter (that sneaks its way to QA or production and is reported as a bug) is due to the fact that I validly implemented a specification one way, when the business need actually wanted a slightly different interpretation of the specification, but just wasn't specific enough when they described it.
Anyway, formal correctness proofs won't handle that. Really all it means is that the hard part of programming - making sure we're actually developing the correct thing - will be offloaded from implementation to specification. That means that implementation will be more of a code monkey role, while the real art of programming - interpreting and anticipating needs, a role that programmers are vastly under appreciated for - will need to be accomplished by someone that is sort of like a product owner, but far more technical and exacting than is the norm now. I'd imagine many senior level programmers would move into that role - translating business needs into formal specification, and then leaving junior programmers to monkey with the proof itself.
I don't see formal proofs replacing acceptance tests. I see them helping you build leak-proof abstractions upon which you assemble the domain where your functionality is implemented. The line between those two positions is blurry and, despite the sound of it, your need to be comprehensive with a formal proof also varies due to possibility and value.
All of these things are just tools after all—you use them to produce value. I think you've described one potential future with this technology, but it, I feel, is very narrow.
One thing that does seem to be playing out is that for many interesting programs the establishment of the theorem is sufficiently challenging that the proof need not be relegated to "junior programmers" but instead automated entirely. Of course, that said, typically a primary tool in the search for a well-specific theorem is a long series of failed attempts to prove its poorly-specified predecessors.
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.
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.
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).
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.
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).