In my previous posting I speculated that compile time type checkers as we know them today may fall by the wayside in favor of something that looks and feels a lot more like the dynamically typed languages.

One of the statements I made, “If you store an object in field foo and then call, y, z), you really don’t care what the type of the object in foo is, only that it should have a function property called bar that can handle the arguments x, y and z.”, needs further qualification.

Yes, you do not care what the type of the object in foo is, nor do you care about the particular function value that is stored in the bar property. However, you do care about what exactly is going to happen when you call, y, z). It is pretty hard to program if you do not know what your program is going to do.

In our current champion languages you get narrow things down by being specific about what types of values you may pass to bar and what type of value you can expect to get back. But that is a far cry from knowing what the function is going to do.

Much more useful is a precondition that states “before you call this function, the following things must be true” and a postcondition that states “if you call this function while satisfying the precondition, you can be sure that the following things will be true”.

Our current best practice is to state these conditions in documentation. Getting this documentation to be accurate and to stay accurate is quite a challenge. And much of the time we never quite get around to creating the documentation.

I am persuaded that a programming language that makes it really easy to write down these pre and post conditions (contracts) and that quickly and accurately checks that function implementations satisfy their contracts, will make programming easier and programmers more productive.

Just how this will be done is not obvious, but it is a worthy goal for anyone aspiring to come up with one or more of the innovations that will unlock the next champion programming language.