4 ms·

Nice set of qualities that make aspects of code obviously correct, but he forgot tests. Like static typing, they are not perfect. They only catch certain clas

Nice set of qualities that make aspects of code obviously correct, but he forgot tests. Like static typing, they are not perfect. They only catch certain classes of errors. But, when you have them, you have the assurance that the code behaves as it does in the test when the same conditions occur in production.

ezyang 15y ago
Disagree. Intuitively, the difference is that an "obviously correct" methodology changes the way you write code, whereas tests don't. Tests have to be run; the mere existence of a test doesn't mean your code is correct. But, crucially, the things a test checks don't generalize. This isn't a perfect dividing line. If you add hooks for DI because you need to inject a mock, arguably that's changing the way you code (this is the schtick of TDD, after all!) Arguably, you have to "run the typechecker" in order to see if you actually have well typed code, and for a sufficiently powerful type checker this might be like running a program anyway. But hopefully the basic gist of the argument is there.
- Locke1689 15y ago
  But, crucially, the things a test checks don't generalize. I think this is the most important thing to note. When I say Example test_fac1: (factorial 3) = 6. Proof. reflexivity. This is completely different from the statement Theorem eq_fac : forall (n : nat), fac n = prod 1 n Tests are simply a mathematical proof of a relation on a specific subset of the domain and codomain of the function. Types, in the broad sense, are constrained proofs over the properties of all elements in the domain and codomain. Types are useful -- they're perhaps the greatest success of formality in software engineering ever. However, they're not complete and completeness is hard. Types succeed because they provide a lot of benefit for very little pain (the constraints you discuss in your post). Your assertion is simply reinforced when we look at the other classes of correctness that we could guarantee. We could write fixpoint definitions for all functions which require structural recursion. We could push all side effects to typed lambda calculus sugar. Fundamentally, we could prove our code correct. But that's a pain in the ass. And it still doesn't work. Tests complement proofs -- they ensure that our own conception of the definition fits our expectations. We could do all the work to formally prove our conjectures, but if our definitions were wrong the conclusions would be useless. What I'm saying is that all of these things should work together -- and the result is a balancing act. We want additional guarantees that our programs are correct, but it requires us to program differently because only certain types of programs have the properties that we wish to exploit. The benefit is that we do have this additional information, so I agree that we should use it.
Chris_Newton 15y ago
> [Tests] only catch certain classes of errors. But, when you have them, you have the assurance that the code behaves as it does in the test when the same conditions occur in production. The trouble is, tests typically don't guarantee to catch an entire class of errors. Rather, each test guarantees to catch one specific case, and when you write your tests you try to cover a useful number of representative cases. This is not to say that executable tests don't have their place, of course, but the plural of "unit test" is not "proof". On the other hand, if you can verify a certain property totally via your type system then executable tests for that property are unnecessary.

ezyang 15y ago

Disagree. Intuitively, the difference is that an "obviously correct" methodology changes the way you write code, whereas tests don't. Tests have to be run; the mere existence of a test doesn't mean your code is correct. But, crucially, the things a test checks don't generalize. This isn't a perfect dividing line. If you add hooks for DI because you need to inject a mock, arguably that's changing the way you code (this is the schtick of TDD, after all!) Arguably, you have to "run the typechecker" in order to see if you actually have well typed code, and for a sufficiently powerful type checker this might be like running a program anyway. But hopefully the basic gist of the argument is there.

Locke1689 15y ago
But, crucially, the things a test checks don't generalize. I think this is the most important thing to note. When I say Example test_fac1: (factorial 3) = 6. Proof. reflexivity. This is completely different from the statement Theorem eq_fac : forall (n : nat), fac n = prod 1 n Tests are simply a mathematical proof of a relation on a specific subset of the domain and codomain of the function. Types, in the broad sense, are constrained proofs over the properties of all elements in the domain and codomain. Types are useful -- they're perhaps the greatest success of formality in software engineering ever. However, they're not complete and completeness is hard. Types succeed because they provide a lot of benefit for very little pain (the constraints you discuss in your post). Your assertion is simply reinforced when we look at the other classes of correctness that we could guarantee. We could write fixpoint definitions for all functions which require structural recursion. We could push all side effects to typed lambda calculus sugar. Fundamentally, we could prove our code correct. But that's a pain in the ass. And it still doesn't work. Tests complement proofs -- they ensure that our own conception of the definition fits our expectations. We could do all the work to formally prove our conjectures, but if our definitions were wrong the conclusions would be useless. What I'm saying is that all of these things should work together -- and the result is a balancing act. We want additional guarantees that our programs are correct, but it requires us to program differently because only certain types of programs have the properties that we wish to exploit. The benefit is that we do have this additional information, so I agree that we should use it.

Chris_Newton 15y ago

> [Tests] only catch certain classes of errors. But, when you have them, you have the assurance that the code behaves as it does in the test when the same conditions occur in production. The trouble is, tests typically don't guarantee to catch an entire class of errors. Rather, each test guarantees to catch one specific case, and when you write your tests you try to cover a useful number of representative cases. This is not to say that executable tests don't have their place, of course, but the plural of "unit test" is not "proof". On the other hand, if you can verify a certain property totally via your type system then executable tests for that property are unnecessary.