3 ms·
And types can’t represent the properties shown by tests. Type checking as typically applied only catches the simple problems of feeding the wrong argument into
by jnwatson 7y ago
And types can’t represent the properties shown by tests. Type checking as typically applied only catches the simple problems of feeding the wrong argument into a function.
Mere mortals can’t construct type systems to enforce most definitions of correctness or licenses or performance.
- cobbzilla 7y agoIt’s not an either/or. Both types and tests help, for different reasons. For programming in the large, both should be used. In the long run it’s about saving time that is otherwise wasted on wolf-fencing and hair-pulling; and in getting new developers up to speed faster.
- jcora 7y agoActually with dependent types you totally can encode proofs that your logic is correct. But I don't really see that trickling down into mainstream programming anytime soon.
- naasking 7y ago> And types can’t represent the properties shown by tests. That's not true generally. Dependent types can be used to represent any property that a test might check, and lightweight alternatives can prove a subset [1]. And this makes sense from the type of logical property being established: you can easily turn a universally quantified proposition into an existentially quantification, but going the other way around means checking all possible permutations of values. However, proving a universally quantification is sometimes (often?) far more difficult than proving an existential quantification, which is why programs have to be structured in a certain way to make them amenable to such proofs. > Mere mortals can’t construct type systems to enforce most definitions of correctness or licenses or performance. Type systems always improve performance, so I don't know what you mean by that exactly. [1] http://lambda-the-ultimate.org/node/1635 http://lambda-the-ultimate.org/node/1635