Ada / SPARK has contracts, too, that can be proven at compile-time. In fact, Ada alone suffices, it has pre- and post-conditions. I think Ada has more libraries

Ada / SPARK has contracts, too, that can be proven at compile-time. In fact, Ada alone suffices, it has pre- and post-conditions. I think Ada has more libraries than Eiffel does. Does anyone even write Eiffel? I am really curious if it is still alive anywhere, in some form.