This is a very nice bug that I stumbled into while running the great auto_test tool on some code I had written. It is a beautiful example of a bug, because it is a very small bug that is still nearly undetectable for the average developer. Also, I do not know about any formal verification tool that could reveal the bug.

The lifetime of an Eiffel program is currently defined by the creation procedure of the root class (normally called 'make' in class 'APPLICATION'). When the creation of terminates, the Eiffel program terminates, too.

There are many discussions on how to make Eiffel type-safe. The ECMA committee has been very active in coming up with solutions (though non of these solutions have been fully implemented and analysed). Most of these solutions evolve around the typing of entities and the rejection of certain polymorphic bindings.