2 ms·
I 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 ques
by tel 13y ago
I 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.