4 ms·
Even with advanced type systems, the sweet spot will be a mix of types and tests. With types, you can prove many claims, including some you can't test for. Wi
by tmoertel 13y ago
Even with advanced type systems, the sweet spot will be a mix of types and tests. With types, you can prove many claims, including some you can't test for. With tests, you can gather evidence to support the claims you can't easily prove with types. So you need both.
Elaboration:
With advanced type systems you can prove that your code satisfies (or fails to satisfy) any property that you can encode as types. The more expressive the type system, the more properties you can encode, and the more kinds of claims you can prove.
But there will always be some properties that cannot be proved or that are too expensive to encode within a given type system. If you care about these properties, you'll have to find some other way of making sure they hold. So, even with advanced type systems, you'll end up writing tests.
The flip side is that there are many important properties that you cannot adequately test for (e.g., "my code is free of injection vulnerabilities"). If you're not using proofs to make sure that these properties hold, there's little reason to believe that they do hold, regardless of how much testing you do. So, even with lots of tests, you'll end up using types.
You need both.
- tel 13y agoI find the decision tree tends to start with whether or not I even understand the problem well enough to generate constraints. After that there are serious questions (today) on whether it's worth formalization. After that, you're probably knee-deep in discovering the difficulty of any proof obligations you've given yourself. Then, finally, you can answer questions about how pervasive the encoding difficulty might be. If those fail at any point it drives you to either use a more permissive type or to just test some useful cases. Not infrequently, test cases can be upgraded into more powerful types.
- contingencies 13y agoIf you test within a small enough scope (even at runtime and without a type system; eg. input to each function, religiously) then you don't really have the "do I understand the problem well enough" architectural issue, which in any event is not something you can test for ;)
- tel 13y agoI disagree completely. Just because you've made an interface doesn't mean it's a good one nor that it will solve your problem. You may also not understand how that interface interacts very thoroughly. Most of programming is figuring out the right interfaces. It's one thing to name a few example inputs and outputs of a single function, it's another thing to think about how a single function interacts with itself (such as what's needed to write a quickcheck property like "for all strings, `reverse . reverse == id`"), it's yet another thing to think about how collections of related functions interact (like seeing some Category laws), and it's a whole set of further things to see all that thoroughly enough to encode it in a logic system.
- contingencies 13y agoErr, I'm not saying understanding the problem is irrelevant. What I'm saying is that it's not an issue that you need to be overly conscious of in testing since it's not something you can test for and properly loosely-coupled code will not exhibit dependencies on architectural assumption.
- tel 13y agoI believe that most of the point of testing is to have a good way to spend time thinking about the problem and the interface you're creating.