The Eiffel language in its current definition has no concept of namespaces. However in large programs using many libraries name clashes (i.e. two classes having the same name) become more and more probable.

Different Eiffel compilers have resolved the name clashes with different strategies. This is not satisfactory because it is not portable.

The following paper describes a proof engine for the Eiffel language.

The proof engine allows the verification of the assertions of Eiffel code. Some language extensions are introduced to express proofs of assertions.

Eiffel in its current form is not completely type safe. Type errors (called catcalls in Eiffel speak) are possible. The compiler cannot detect these type errors. They usually trigger an exception at runtime.

These type errors are possible due to covariant redefinition of arguments and polymorphy. Both principles are very powerful in OO programming.

There are 4 deferred classes defined in ELKS to represent agents

  ROUTINE  [BASE_TYPE, OPEN_ARGS->TUPLE]
  PROCEDURE[BASE_TYPE, OPEN_ARGS->TUPLE]   
  FUNCTION [BASE_TYPE, OPEN_ARGS->TUPLE, RESULT_TYPE]
  PREDICATE[BASE_TYPE, OPEN_ARGS->TUPLE]   

The OPEN_ARGS is tuple to represent the tuple of arguments which need to be provided at call time.