Not enough
Let’s start with a premise, indulge me if you please:
- You’re creating a system for some client
- You’re using a dynamic programming language like Clojure, Ruby, Io, etc…
How do you know your system works properly? One answer is that you write unit tests. However, as Evan Farrer wrote in his excellent blog post, “Unit testing isn’t enough. You need static typing too.”. I think this he’s absolutely correct; unit testing is not enough. But…
Static typing is not enough. You need contracts too.
However, while static typing will catch a very large class of errors that you may never discover with unit testing, they will not catch everything. There are a certain class of errors that are caused by subtle, broken relationships between inputs to any given function or method and their results. This is where contracts can really save you.1
Contracts are not enough. You need generative testing too.
But how do you know that your contracts are valid? That is, how do you know that you’ve identified them all? Likewise, how do you know that the contracts that you’ve specified are consistent? One way of tackling this problem is a class of verification where tests are either inferred directly from the contract specifications, or you may need to use a limits specification language to effectively restate the contracts. In either case the intent is to target the assumptions of functions and methods with a mass of data inputs.
Generative testing is not enough. You need simulation testing too.
So you’ve written specifications (or had them inferred) that validate that your local assumptions hold true. What about the behavior of the system as a whole? It’s unlikely that generative testing will provide help there. Instead, another approach may be to create a testing harness to simulate parts of your system talking to other parts in different aggregations up to the level of the user interacting with the system qua system. The power in this approach comes ex post-facto. That is, I assume you would collect system activity into some external store that is then independently verified for accuracy.
Simulation testing is not enough. You need fuzzing too.
I hope that you remembered to cover more than the happy path in your simulation tests. If not, then you probably missed the opportunity to check if your system works in the presence of massive chaos and confusion (i.e. the real world). Fuzzing should help you here.
Fuzzing is not enough. You need luck too.
In my experience, there is no such thing as luck. — Ben Kenobi
The odd thing about fuzzing is that it may not hit on the magical incantation that breaks your system. That’s the problem with randomness; you can never be sure.
Luck is not enough. You need user testing too.
What if you created the wrong system? You may have observed every step in this post, but what you’ll have created is merely a verifiable piece of garbage.
I hope the intent of my post is clear.
In software development, no one thing will save your ass.2
This is daunting to say the least. In the face of all of this complexity3 and uncertainty why on earth would anyone willingly become a programmer?
The answer is simple.
All you need is love.
Love Driven Development.
:F
-
The programming language Agda is exploring some extremely interesting techniques that may even allow one, with the proper encoding, to move many of these contractual consistency checks into the realm of static analysis. ↩
-
And sadly, doing all of these things may not save your ass either. ↩
-
And this is far from a complete list. ↩
21 Comments, Comment or Ping
david karapetyan
Prototype in a dynamic language and then move bits and pieces as necessary into a statically typed one and pepper it with all the goodness that comes with static types. That’s the workflow I follow and it works out pretty well. It would be nice if I didn’t have to switch languages but I’m not aware of any significant push from academics or practitioners for “optionally typed” languages that mix and match the best of both worlds.
Jun 20th, 2012
Sam Tobin-Hochstadt
Fogus, I couldn’t agree more (although Agda is far from the only player in the verified software space).
David, lots of people are working on exactly this. If you click on my name, you can read about my work on Typed Racket, which supports exactly what you describe.
Jun 20th, 2012
Jeff HeonJfheon
@David I feel obligated to mention the Fantom Programming Language. Often dismissed as only being used for targeting both .net and the JVM, but a nice language on its own featuring optional static typing and modularity. Also targeting the browser for a round trip in the same language and various other interesting philosophy decisions. See. http://fantom.org/ and http://fantom.org/sidewalk/topic/1581
Jun 20th, 2012
William Payne
We are still living in the dark ages of our craft; I look forward to a bright future where, out-of-the-box, our programming tools support, encourage or enforce the sort of testing detailed in this post.
However, as Fogus suggests, testing alone is not enough. The program itself sits on the other side of the reliability coin.
Too often, we dig our own graves by creating over-engineered, overly complex systems. We take this path either blindly slipping, incremental change by incremental change, or arrogantly, abrogating the humility that is necessary to maintain the discipline of simplicity that is so very necessary.
Jun 20th, 2012
Kevan Benson
One of the main (as of yet unimplemented) features of perl 6 is an optional type system for verifIcation and optimization. Obviously it’s not unique in the regard, but if you want to try your hand at implementing such a system, I’m sure they would love the help. ;)
Jun 20th, 2012
Eric Seidel
I think you can make a stronger statement, “In software development, no sum of things will save your ass.”
Even if you could verify that your program is 100% correct (via proofs, tests, or whatever else you felt like throwing at the problem), you’d still be at the mercy of the people who created the compiler/interpreter you’re using and the hardware your program is running on.
And yet, even with what seem to be insurmountable odds in the way of writing correct software, I can’t imagine wanting to do anything else :D
Jun 20th, 2012
John Weber
@David Check out Common Lisp. It’s an optionally typed language, as well, although it’s not as thorough as haskell. Unlike other optionally typed languages though, it’s actually well known, widely used, and mature.
Jun 20th, 2012
Fosco Marotto
How about “No amount of buzzword best practices will guarantee anything… just build it, test it, and move on.”
You don’t necessarily need any of that stuff, if what you build works, and no lives are at stake.
Jun 20th, 2012
eMBee
david: that’s why i use pike. it supports static types at compile time and dynamic types at runtime. the compiler can be told to ignore the type by declaring variables as “mixed”, and then later when you know what the types are change them to be specific.
greetings, eMBee.
Jun 21st, 2012
Innocent Bystander
You mean like Lisp has had since at least 1985?
(declare (type …))
You can specify types as much and as little as you like.
Jun 21st, 2012
Andrew Traviss
Flash went from fully dynamic to using optional typing when Adobe introduced the new virtual machine and JIT for Flash Player 9. After using it this long I have a hard time understanding why optional typing isn’t more common in mainstream languages.
Dynamic and static typing are both good tools and having to hop between languages to choose between them seems obtuse.
Jun 21st, 2012
Vagif Verdi
The problem with your post is that you are stating useless truisms. It’s like saying “wearing seatbelt is not enough, the meteorite may fall on your car.” In other words you are not taking into account the Point of Diminishing Return.
Static typing offers huge and visible return for performed work. Anything else though quickly drops to the level of statistical error rate.
Jun 21st, 2012
fogus
@Vagif
I think this is true to some extent, but there are many errors that static typing will not catch, but these other types of verification strategies will. What does that buy you in the face of attempting to prove that your system can run with two simultaneous users? How does the type system prove that it can withstand a DoS attack? Likewise, how can it prove that your system properly handles the case where the user types some garbage into a textbox? How does it help prove that your system keeps running if someone pulls the network cable out of the wall? How does it help prove that you wrote the system that your client wanted?
None of these conditions are statistical noise; they are harsh realities of writing software. Maybe your systems are not subject to these types of realities, but many systems are and static typing is only one of possibly many tools to help in the fight.
Jun 21st, 2012
Vagif Verdi
@fogus
You are confusing the insufficient knowledge of a problem domain with programming errors.
All your examples are just that. And no tool, not even your contracts can save you from DDOS attack if the programmer is not aware about them :)
The programmer errors though are the ones that have nothing to do with a problem domain: typos, wrong types, wrong conversions, missing branches (non exhaustive case statements), boundary checks etc.
Jun 21st, 2012
fogus
Hold on a sec. This is my blog and I wrote about all kinds of errors and validation techniques. You keep wanting to focus on static typing. :p
Jun 21st, 2012
Tim Jones
@vagif
IMHO being a programmer is more than slapping bits together. A system which does not crash the machine, compiles, and passes unit tests is worthless if it does not do what it is supposed to. Programming is a holistic art, which I think is part of the point of this post (and why static typing, etc. is not enough).
Jun 21st, 2012
Vagif Verdi
@Tim Jones
That’s a useless point. It does not give us any insights on how fix the situation or what is there need to be fixed.
It’s no different than saying “You can’t prove god does not exist”. Yes, so what ?
The fact of the matter is: There are the same mistakes programmers do again and again. Those mistakes can be prevented by modern tools (static typing, unit tests etc).
And there are mistakes programmers make simply because they do not have enough knowledge and make the wrong decisions. These cannot be solved by any tools, no matter how much you pile them up.
Jun 21st, 2012
un_passant
Excellent post as usual !
Thanks for pointing out Agda. You sparked a very interesting discussion with some of my coworkers, and I discovered mini Agda [*]. As I know that you have a thing for toy languages, I thought that you might find it interesting (if you did not already know about it).
Cheers !
[*] http://www2.tcs.ifi.lmu.de/~abel/miniagda/
Jun 22nd, 2012
Tim Jones
@vagif
I’ll try to be more precise.
The situation is simple. Writing correct software is difficult. The practices in this post outline some ways to mitigate the fact of incorrect software.
Great. I use these tools myself. However, the programmer’s job does not end there, which is why I disagree with your assertion that:
As fogus said, this may be true in some domains, but in my experience (limited though it may be), “anything else” has been critical to success. And whether it’s part of a specific domain or not, the errors these other practices address are something programmers must deal with or else they have failed to do their job correctly.
Perhaps, but we have to try! (I think that’s where the love comes in.) You can’t say “I have my unit tests and static types so I’m done.”
What’s your point? Don’t do these other practices b/c they might not matter? Programming w/o static types is foolish?
Jun 22nd, 2012
david karapetyan
@Everyone: Thanks for the pointers. I should have been more specific and said that I don’t really want to give up the goodness of all the “intellisense” technology offered by microsoft and eclipse and I want the tool I use to offer all of this in one integrated whole. I know I’m a pampered weenie.
I’ll take a look at the languages mentioned and what infrastructure they offer for streamlined development.
Jun 22nd, 2012
Eugene
My contribution to Love Driven Development: https://github.com/jamm/LOVE
Jun 30th, 2012
Reply to “Not enough”