Lambda the Ultimate

The article talks about modules in Modern Eiffel (a variant of Eiffel which allows static verification).

The main points are

1. integration of functional and object oriented style

2. physical separation of specification and implementation

ad 2: This separation is not only possible for functions and procedures, but also for assertions. I.e. the specification part includes only the assertions. The proofs can reside in the implementation part of a module.