Why Type-safety?

The search for a type-safe version of Eiffel is a never-ending story in the development of the Eiffel language. Recently, Helmuth Brandl has created a series of blog entries with a nice description of is needed to make Eiffel type-safe. There have been others posting blog entries (including me) and it also had been a constant topic during the ECMA process of Eiffel standardization.

Interestingly, a question that was seldom raised was: why do we need type-safety? As absurd as it seems for all the mathematicians to raise this question, the Eiffel community has understood for a long time that mathematical soundness is not a reason in itself. Instead, it serves a purpose in the enterprise of language design: giving software developers means to express themselves in ways that reduce the number of defects in his/her programs and enable him/her to master complex problems he/she would not be able to master without.

In Eiffel, the defects in the type system allow the developer to write code that creates so-called CAT calls. If you are lucky, CAT calls will crash your program. If you are unlucky, your broken code will continue running and corrupt your data. The theoretical consequences of CAT calls are severe.

In practice, I have rarely had problems with CAT calls. For all the code that I have written and encountered in the last years, CAT calls have only been one out of many possible sources for defects, and even then a minor one. CAT call detection in some of the Eiffel compilers has helped as well.

The amount of effort put into making Eiffel type-safe has been completely disproportional to the amount of actual CAT calls it produces.

So, if so many people are interested in making Eiffel type-safe, and at the end CAT calls are such a small problem, perhaps there is a different reason for type-safety that we have to take into account!

I claim: a type-safe language will capture design bugs! It is not about making the software not crash. It is about creating consistent designs that make it easy to reason and properly abstract the problems into a hierarchy of classes. For example, had Eiffel had type-safe Genericity from the start (allowing invariant, contravariant and covariant arguments), the design of many libraries, specially of EiffelBase, would have been much better and more consistent.

For a software developer who has worked with program verifiers, I know what an enlightening experience it is when the verifier slaps your hands and shows you what you did not understand in your own design in the first place. Following Mark Howard’s keynote of TOOLS 2007, the type system is indeed a light-weight prover. Provers are great to show you where you just had not properly understood the problem. And they show no mercy doing so ...