Some months ago I have started a blog about static verification of software.

The blog already contains a significant amount or articles like "Functions, ghost functions and higher order functions", "Framing: An approach to mutability", "Introduction to the proof engine", "Proof procedures" etc.

For those of you who are interested in this topic, you can check it out at http://softwareverifica

Main features of Eiffel

The main features of Eiffel are:

- clean object orientation with multiple inheritance

- design by contract

- elegant expressive syntax

- automatic memory management

- generics

- uniform type system with type safety (exept catcalls)

These features were unique at the time Eiffel was invented (some 25 years ago).