4 ms·

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

by 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.

by ezyang 15y ago

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.