There have been some great posts recently going around about the merits of static vs dynamic languages ...

Dynamic Languages Strike Back by Steve Yegge

Return of the Statically Typed Languages by Cedric

I have to admit that I was really waiting for the Java/C# "Attack of the Clones" reference...

Which are then summarized and moved towards polygot programming by Ola Bini in A New Hope: Polygotism.

Quoting Ola's summary:

So let's see. Distilled, Steve thinks that static languages have reached the ceiling for what's possible to do, and that dynamic languages offer more flexibility and power without actually sacrificing performance and maintainability. He backs this up with several research papers that point to very interesting runtime performance improvement techniques that really can help dynamic languages perform exceptionally well.

On the other hand Cedric believes that Scala is bad because of implicits and pattern matching, that it's common sense to not allow people to use the languages they like, that tools for dynamic languages will never be as good as the ones for static ones, that Java generics isn't really a problem, that dynamic language performance will improve but that this doesn't matter, that static languages really hasn't failed at all and that Java is still the best language of choice, and will continue to be for a long time.

On a side note Cedric has a big point on the tooling side of dynamic languages; it will never be there as it can't be logically. Since so many things are dynamic at runtime I will eventually end up running into the halting problem trying to figure out what happens at runtime.

I think however that this entire discussion of static vs dynamic languages is fundamentally flawed as shown later in Ola's post when he describes the debate as:

So, we have three categories of languages here. The strongly statically checked ones, like Haskell. The weakly statically checked ones, like Java. And the dynamically checked ones, like Ruby.

It seems to me to be rather silly to have this discussion of static vs dynamic languages without bringing in the concept of static verification of more than just types.

Enter DbC

E. W. Dijkstra arguably one of the most influential computer scientists of our time recognized the importance of static verification and the provability of computer programs. In "The Cruelty of Really Teaching Computer Science" he even went so far as to make a proposal for an introductory programming course for freshmen that consisted of Hoare logic.

There are languages out there that do more than verify just your types. Most of them currently are in the lineage of of Betrand Meyer's Eiffel programming language and can be considered DbC (Design by Contract).

Sure DbC is pretty obscure now but it is a hot area of research due to the ability to use theorem provers on the contracts of the system. These theorem provers are not looking solely at type safety in a statically verifiable way they are also looking at your code and contracts to be sure that they cannot be broken at runtime! This is not a new idea (research in this area goes back to the beginnings of DbC) but the exponential growth of processor and memory resources have made this a much more obtainable goal. There are now two fairly mainstream projects working on this now, the JML (Java Modeling Language) project and the Spec# project from MSR.

Their working is best seen in an example (although this is an extremely naive example, for more in depth examples check out the samples in the spec# install)

using System;
using Microsoft.Contracts;

public class Program
{
  static void Main(string![]! args) {
      Console.Write("Entry? : ");
      string response = Console.ReadLine();
      Console.WriteLine(response.Substring(response.Length - 6, 6));
  }
}

This code will give 3 compile time errors.

C:\crap\Project1\Project1\Program.ssc(9,22): warning CS2663: Call of string.Substring(int startIndex, int length), unsatisfied precondition: 0 <= startIndex
C:\crap\Project1\Project1\Program.ssc(9,41): warning CS2663: Possible null dereference
C:\crap\Project1\Project1\Program.ssc(9,41): warning CS2614: Receiver might be null (of type 'string')

Note that you can treat these as errors as well (and they show up in the ide as normal errors).

These errors result from two basic problems with the code. The first problem is that Console.ReadLine() may return null in which case the Substring call and the Length access would cause problems. The second problem is that the length of the string returned from the ReadLine may be less than 6 in length. By placing some defensive code we can prove to the prover that we understand and are handling those cases.

using System;
using Microsoft.Contracts;

public class Program
{
  static void Main(string![]! args) {
      Console.Write("Entry? : ");
      string response = Console.ReadLine();
      if(response != null && response.Length >=6) {
            Console.WriteLine(response.Substring(response.Length - 6, 6));
      }
  }
}

Which will give no errors as the spec# compiler parses the code and understands the branching enough to realize that I have now proven that those bad circumstances can no longer happen. The key thing to notice here is that even without unit tests it is finding problems in terms of verification of my code (I said my code runs within these rules and I am breaking my own rules). These tools will REVOLUTIONIZE the development industry.

Note: These contracts do not get rid of things like unit testing or TDD they complement them. There is a difference between verifying (Do I play by my own rules that I set up) vs validating (does this thing do anything of value)

There are many scenarios where this can benefit us but one of the main ones I see is in dealing with invariants that deal with multiple methods and/or objects (these are often very difficult to unit test). A simple example of this can be seen in List<T>, in particular there is an invariant between List<T>.Count and the number of items in a List<T>. These tools will allow you to make it so you can insure mathematically that this invariant is never broken as opposed to sprinkling around state based tests and hoping that you actually covered all of the places where the invariant is being accessed. These problems are obviously magnified when we introduce an invariant that spans multiple objects ...

Another scenario where theorem proving can help us greatly is in our refactoring. The compiler will not let us break our previously distributed contract providing we don't change it. To provide the same level of support with unit tests tends to cost us many unit tests for complex contracts with many preconditions.

Does DbC play well with others?

Coming back to the concept of polygot programming; it is reasonably easy with dynamic and static languages in general as can be illustrated by the existence of the DLR. There is however a much larger disconnect between the world of theorem proving and dynamic languages. Dynamic languages are in their definition runtime defined and static verification is in its definition compile-time defined, the use of a dynamic language makes the concept of statically verifying your code at compile time impossible. To try to verify dynamic code at compile time would likely walk you straight into the halting problem just like it would for many kinds of tooling.

I took some time at alt.net seattle to pull aside Mike Barnett and Rustan Leino from the spec# team and John Lam from the IronRuby team to talk for a few minutes on video about how we can effectively use these ideas together. Many interesting ideas came out of this discussion in particular the recognizing of the merits of dynamic languages for change and the possibility of starting in dynamic languages and annealing software into compile time proven languages. I have submitted this video and am hoping it will be coming out soon!