Reg Braithwaite been after me to stop going on about static typing and say something deep about programming. I’ve been trying, really I have. But then he has to go and post something like like this, which then forces me to stay up late and respond to him, as it’s obvious he hasn’t gotten what I’ve been trying to say. Which makes me cranky.
And while Reg may try to cop a plea by saying:
I am not saying that strong typing or provability, iterative development or BDD, or anything else is necessarily better or worse in this respect.
Unfortunately, the original posting was very much about, and very much anti, static typing:
This is somewhat more obvious with an example. Suppose I asked you to write a program that could break a CAPTCHA. Writing the program is very time consuming and difficult. But first, before you write the program, what if I asked you to write some tests for the program you will write. That’s trivially easy, isn’t it? You just feed in some CAPTCHA images and then check that the program spits out the correct value. How do you know your tests are correct? You apply the red-green-refactor cycle along with the principle of triangulation. ;)As we see, testing is easy. So how do you prove its correctness? Is it as easy as testing it?
OK. Now go and write a test suite that demonstrates your program doesn’t have any race conditions. I’ll wait.
The thing is that there are two meanings for a program being “correct”- and both Reg and Phil Haack are confusing the two. There is the definition that a program is correct when it does what we (or the customer) need it to do, and there is the definition that a program is correct when it does what we the programmers meant it to do. The second meaning is a significantly weaker proposition, no argument- it is possible to write a perfect, bug free program that simply doesn’t solve the problem, or any problem.
All static typing- and unit testing, for that matter- do is help ensure the program does when I mean. That’s all. But that’s important, because the more time we the programmers have to spend making sure the program does what we mean, the less time we have to spend on figuring out what it is we want the computer to do. What means we’re more likely to get to the “does what we want (and what we mean)” nirvana, and more likely to get there faster.
This is the point where Reg will hopefully go “hmm”, and wander off to think about what I’ve said. Me, I’m off to bed. Good night.
10 Comments
“This is the point where Reg will hopefully go “hmm”, and wander off to think about what I’ve said.”
Ever the optimist huh? The problem is he doesn’t want to think about what people say, he wants to dismiss it off hand. Its the attitude that if static typing doesn’t solve EVERY problem, then its not worth having. Just because you can still write the wrong software with static typing, doesn’t mean its not helpful to at least write the software right, giving you more time and brain power to worry about making sure its also the right software. And just because you can’t prove that a program does what the customer wants, doesn’t mean formal verification is useless. Its still nice to prove things like that there are no integer overflows, no out of bounds array accesses, etc.
I think it’s pretty harsh to say that Reg dismisses stuff off-hand. He’s responded to posts with insightful “clarifactions” and self-corrections before, including responding to posts on this blog.
Maybe I am just a pessimist ;) But it seems that if he was really willing to consider things, he wouldn’t still be posting the exact same “static typing doesn’t solve some other problem and make all programs perfect all the time, so its no good” strawmen still.
I think his position is a bit more nuanced than what you’re giving him credit for — he has said some surprisingly nice things about OCaml, for instance…although admittedly, only after prompting and even then he’s defensive about being a dynamic coder (“So that’s why dynamic languages in conjunction with automated test suites are working for me.”).
Speaking of which, I’ve been meaning to rant about “The nice thing about grammar errors is that you don’t have to try very hard to catch them. If you have reasonable code coverage, you’ll find them.” for a long time…
The post you quote says nothing about static typing for the simple reasons that I was not thinking about static typing at all when I wrote it.
I will now tell you exactly what I think of static typing, so there is no confusion. Ready? I think it is useful for software development.
Please do not equate my post with Phil’s, whether you think him correct or not. I quoted a specific passage I found interesting. I have written before that I can find a post–including this one I am responding to right now–interesting and informative without agreeing with it in its entirety.
I was not confusing “does this program do what the programmer intends” with “does this program do what the customer wants.” In fact, I was drawing the distinction in the article and stating that I believe the latter is a means to achieving the former.
In that respect, I believe that static analysis of programs to detect inconsistencies (a large field that includes static typing) is useful.
You may not know this, but I used to write code analysis tools for Java server applications. I somehow wonder why you insist on portraying me as an “all or nothing” person when both my actions and my words express an interest in a wide variety of programming tools and techniques.
I am going to challenge you now. I am not trying to provoke a fight, I honesty want YOU to go away and say hmmm. Why is it that you are trying to paint me as such an absolutist, that when I say “I like static typing but I’m currently achieving my personal goals with a dynamic language” that I must be against static typing?
The question I put to you is this: could it be that YOU are the one who sees the world in right and wrong, black and white, correct and incorrect? If that’s the case, there is nothing wrong with your beliefs. I am not saying you should relax and blur the lines between good and bad in your mind.
But I would encourage you to consider the possibility that others, such as myself, are not as rigid in their mindset. I’m very proud of the work I’ve done using some extreme “type torture” in C++ to impose constraints on programs. I’m also very proud of some of the work I’ve done in Ruby. I have no difficulty embracing each in its own way.
After all, one roadhouse can host both kinds of music, Country AND Western.
You’re going to make the youngsters scratch their heads with those old Blues Brothers references, Reg.
Static typing: most useful when party A does not understand party B’s software as well as they should (or would like). It’s a great way to catch conceptual errors quickly. And if you’re coming and going between different tasks and code areas, conceptual errors pop up all the time. So it’s good for multitaskers.
In my experience, once you get really facile with a library or an API, the static typing seems to just get in the way.
@jb
The Blues Brothers are forever.
If you’re finding that static typing “seems to just get in the way”, then you need to get into a language with a better type system. I’ve never been annoyed with OCaml’s type system from a user’s standpoint (which is more than I can say with Java: cite, cite), mainly because it supports duck typing, so I’m whipping out code at the same rate as I can whip out Ruby.
That said, there is some chattiness for the original author which would be nice to go away, and may be what you’re talking about when you say “get in the way”. Some of this is avoided by auto-generating *.mli files, and some of it can be solved by free-wheeling a bit more with the structural typing, which is something I have trouble letting go of.
re: The Blues Brothers
I chose that quote because I think that two people comparing and contrasting Ocaml vs. Ruby probably have a lot in common.
I think the comment about race conditions is silly. Imagine it written thus:
“OK. Now go and write static type declarations that prevent your program from having any race conditions. I’ll wait.”
So your “can’t do it” example ends up cutting both ways. Typical languages don’t have declarative lock-taking (it’s all imperative code) so they can’t have any declarative means to make assertions about those locks. It also seems like if the compiler has enough knowledge to check deadlocks and race conditions, then it has enough knowledge to take locks for us in the first place, and we wouldn’t have to worry about it ourselves.
My apologies for not responding sooner- I was away from the net for a while. And apologies for writting a long response- I didn’t have the time to write a short one.
Reg first:
Guess what? I’ve been doing most of my programming recently in Perl. For the things I’ve been doing- reading simply structured text files (csv, pipe seperated, fixed length, etc.) and tossing them into a database, or connecting to the database and firing SQL at it, or reading data from the database and spitting out simply formatted files, perl has a lot to recommend it, and is a better tool for the job than Ocaml. Ocaml would be better than Java or C++ for this job, but that’s damning with faint praise, IMHO. So, by the criteria you’re using to paint me as painting you as an absolutists (which is working, by the way- see Steve Vinoski’s blog), I too hate static typing.
Um, right.
I’ve gone and reread all three posts posts (yours, mine, and the original) just now. And I did paint with too broad of a brush, and I apologize. In my defense, I was a) tired, and b) had passed up commenting on the original article, thinking “Reg is already on my case about flaming about static typing, and if I respond to this one he’ll be right”. But then you went and called the article “The best question asked this week”, and I let fly. But for the original posting, I was spot on. Consider the following quote:
It’s hard for me to interpret that as anything except being anti-static-typing (static typing being a weak form of code proofs, and there being a very strong cross over between the Hindley-Milner static typing crowd and the code proofs crowd).
The bigger the system, the more important I feel static typing, and at the extreme even code proofs, are. Proofs that the code does at least what is it intended to do, even if it doesn’t do what it needs to. Because the larger the system, the more likely there will be unintended interactions, and the greater the complexity. Frankly, we humans suck at writting programs that do what we intend them to do, in all environments and for all inputs. Mostly does what we intend it to do, in most environments and with most inputs, yeah. Occassionally, and with heroic effort. But most programs are riddled with memory leaks, security holes, crashes, corruption, and just general suckiness.
And, by and large, most programmers don’t admit that- and don’t admit that there is any thing computer science- the actual academic stuff- might have to teach them about making programs that don’t suck quite so badly. In fact, many programmers are not just indifferent to theory, they’re outright hostile to it. You don’t have to spend too much time on slashdot to find this hostility, and it shows up even on digg and reddit. In either case, huge tracts of theory are not only not know by most programmers, most programmers don’t even know it exists.
While I’m on the subject, Saphirecat, go take a look at Software Transactional Memory. Haskell has done exactly that, used it’s type system (and purely functional programming)_to allow it to prove that there are no race conditions. Ocaml doesn’t have this, but that’s because Ocaml isn’t that advanced of a language- the core of Ocaml (the Caml language) is 20 years old (Caml predates Java), and SML, the language Ocaml is based on, is over 30 years old (SML is older than C++).
But this hostility to theory is having a cost. As Java seems to have been nominated the ultimate in “theory” languages by the theory-hostile, the industry as a whole is undoing what little help theory has played in making programming more usefull. It’s not just typing- Java’s GC is almost as bad (I have a post brewing on that). GC doesn’t have to be complicated and slow, people.
But this has given me something of an itchy trigger finger on the subject- especially considering I too was once an ignorant sot. I learned Ocaml because I had set out to write “a better Java than Java”, and people kept telling me that I should learn a functional programming language, as it’d improve the language I was designing. To make a long story short, I learned Ocaml, which turned out to be (in every possible way) a better language than what I was designing, so my language went the way of the smallpox virus (extinct and not missed). You can probably scare up some good quotes by me from my days on comp.lang.java.advocacy, if you’ve a mind to.
2 Trackbacks
[...] from this comment Reg made on another blog, it seems that he’s being accused of being an absolutist, in this [...]
[...] What are you trying to prove? [...]