A brief point on static typing
This post also incidentally attempts to justify my answer to a question that I regularly encounter, what is your favourite programming language?
It’s not possible to write bug-free programs.
This particular myth is quite popular, and its recent inclusion in a discussion I had has prompted me to write this post. The profound fact of this matter is that this statement is “as false as you can get.” In other words, there exists a formal proof of its negation, and subsequent counter-examples. It has also been my experience that belief in this myth has degenerative practical implications.
To emphasise the point, there exist programming languages for which it is impossible to write an incorrect program. What does it mean for a program to be correct? It means the program terminates. Such languages include (in order of my decreasing experience with them): Coq, Agda, Epigram, Isabelle.
Some people like to think “correctness” includes the thoughts of one or more persons in order to make the assessment. For example, one might proclaim, “sure you have a proof of program termination, but that is not the program that I asked for!” I think this is a poor use of the term “correctness” and I am not considering it any further here.
There is a problem with the aforementioned programming languages. A big one. While you always have correct programs in these languages, you cannot have all general programs. This is a well-documented contention. So you might say that these languages set out to achieve the objective of emphasising correctness, but at the expense of generality — in other words, they are exploring the question: “just how general and practical can we get, without sacrificing absolute correctness?” In my opinion, this is a very important question and worthy of further research.
Other programming languages sacrifice correctness for generality. In my typical work (I work for a product company), this includes languages such as Haskell, Scala and even Scala’s type system (which can be used as an embedded language). I expect most of my readers fall into this category of usage of languages. That is, we are all using languages that explore the question: “just how correct and practical can we get, without sacrificing generality?” In my opinion, this is a very important question too.
In the pursuit of answering both of the above questions, there are a number of contentions that arise. This means that there is not a holy grail programming language. It also means that there is a lot to understand before even starting to talk about the merits of correctness (aka static typing). This is unfortunate given the strong compulsion for, and quality of, popular commentary — we spend too much time clearing up myths. I digress.
However, this issue of contentions and trade-offs does not preclude the existence of questions of dismissal of programming languages. That is, it is possible to ask, and even answer, the question of whether or not there are programming languages that offer nothing toward resolving all of these (meaningful) contentions with respect to peer programming languages. These programming languages may be dismissed as offering nothing toward the goals of computability. It may be said that they are “universally impractical” with respect to the goals of computability (I am explicitly distinguishing here from social objectives). This may seem pessimistic, but it’s just a fact of the matter.
I hope that helps.
March 26th, 2011 at 1:51 pm
Hi Tony,
I don’t believe you’re using the term “correctness” in a standard way. A program is “correct” with respect to a specification, like one given in a Hoare triple. Termination isn’t enough to ensure correctness. The program must terminate *and* satisfy some postcondition. (See, for example, Understanding Formal Methods p. 18-19). “Strong normalization” might be a better term for what you’re describing. Coq’s specification language has this property in that all programs written in it terminate in a normal form.
With respect to mixing expressivity with strong normalization, I agree that’s a worthy goal. There are several such projects underway. Trellys is one (http://code.google.com/p/trellys/), allowing general recursion with a sub-language that is still consistent and strongly normalized.
Yuvi
March 26th, 2011 at 3:35 pm
Yuvi, you’re right and I apologise for the inaccuracy.
March 26th, 2011 at 4:51 pm
Though I believe you’ve successfully countered the claim that “it’s not possible to write a correct program”, for one possible completely valid definition of correct, I have yet to be convinced that “correct” and “bug free” are truly synonymous.
The term “bug-free” indicates the absence of any undesirable behaviour, there’s even a large category of software (web sites, network switches, etc.) where the goal is to run continuously with preferably no downtime whatsoever. In these cases, termination is the very antithesis of “bug-free”
March 26th, 2011 at 8:15 pm
Kevin,
Using a web application as the example, write it in such a way as you can (aspire to) prove the sub-program. The “running forever” part becomes largely irrelevant.
March 26th, 2011 at 10:33 pm
When people say “It’s not possible to write bug-free programs.”, I assume they really mean “In practice, in the languages we use, it turns out that I, and most other people — including known great programmers –, are incapable of writing bug-free programs”. That is an undeniable truth, but it can’t be used to justify having bugs in your code, because better programmers introduce fewer and ’simpler’ bugs, independent of the language.
March 27th, 2011 at 2:23 am
I’m with Kevin on this one. A bug is an undesirable behavior in a program. Not being correct qualifies as a bug, but by no means comprises it.
March 27th, 2011 at 4:09 am
Hi Tony!
This somehow reminded me of this: http://james-iry.blogspot.com/2010/05/types-la-chart.html
Where I really liked the diagram to visualize the different properties of programming languages in this context.
regards Andreas
March 27th, 2011 at 8:08 am
What if there’s a bug in Coq?
March 29th, 2011 at 6:42 am
There’s a trend here: we discard untyped programs and we get less bugs, we discard uncontrolled mutation and we get less bugs, and now we discard uncontrolled recursion and we get less bugs.
) that the future of programming lies along the line of Coq et al, and “programming” should be called “applied logic”. When you just need to tinker and you don’t care about correctness, something like Visual Basic should be enough 
Maybe the loss of generality is not that big…
I believe (or want to
Last year I took “Formal Program Construction in Type Theory” at my Uni, it was a small “tour de force” with Coq and it blew my mind.
March 29th, 2011 at 9:25 am
A more obvious, and less controversial, example, would be your simple “Hello World!” program, which presumably can be programmed and then proven to be correct with little difficulty…
March 29th, 2011 at 3:52 pm
rzezeski: guess what? There are bugs in Coq - for the curious, their bugzilla URL is below.
However Coq has grown rather large and contains stuff far beyond what is strictly necessary for minimal useful programming language.
At its core, it’s based on formal system (’Calculus of Inductive Constructions’), with set of axioms proven to have necessary properties. That proof is informal, but published and peer-reviewed - that’s as bug-free as one can get in mathematics.
Over the time, various efforts were made to ‘bootstrap’ Coq - that is, implement and prove correctness of Coq in Coq itself. I don’t know how far did they get.
http://coq.inria.fr/bugs/buglist.cgi?query_format=advanced&short_desc_type=allwordssubstr&short_desc=&product=Coq&version=8.2&long_desc_type=substring&long_desc=&bug_file_loc_type=allwordssubstr&bug_file_loc=&bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED&emailassigned_to1=1&emailtype1=substring&email1=&emailassigned_to2=1&emailreporter2=1&emailcc2=1&emailtype2=substring&email2=&bugidtype=include&bug_id=&chfieldfrom=&chfieldto=Now&chfieldvalue=&cmdtype=doit&order=Importance&field0-0-0=noop&type0-0-0=noop&value0-0-0=
June 20th, 2011 at 7:56 pm
Interpreting (think misconstruing) informal statements like “It’s not possible to write bug-free programs.” in a formal way is a sure way to arrive at some counter-intuitive result.
How about “It’s raining outside.”. The truth depends (not only) on the definition of outside. Is the whole world “outside”. Then this proposition is probably true all the time (ok, ignore granularity of time for now). If we define “outside” to be only the first centimeter off the walls of a building; well that’s probably covered by the roof and chances are that it’s only raining _there_ when it’s also very windy.
In both cases we arrive at counter-intuitive intrepretations when trying to formalize an informal statement. That’s nothing new.
The same has happened with your formalization of “correct”. I’m sure you’re totally aware of this fact.
As a side note: A proof may be correct — but it may proof the wrong thing (something useless). Then it will be of little worth.
June 21st, 2011 at 4:37 pm
When I see “It’s not possible to write bug-free programs”, it’s usually a deeply-held belief that projects as “I have a history of writing programs with bugs.” There isn’t any requirement to depend on alternative definitions here — the claimant is simply wrong — at least in my experience.