Reasoning with inductive types

Modern Eiffel is a new language which is syntactically based on Eiffel but has a lot of concepts of functional languages like Haskell, OCaml or Coq. Modern Eiffel puts the emphasis on static verification, i.e. a compiler can statically check that a programm written in Modern Eiffel meets its specification.

The following article describes how Modern Eiffel's proof engine can be used to reason with inductive types.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Does Modern Eiffel exist?

Does Modern Eiffel exist? I can only find a few blog entries and what seems like an informal "Modern Eiffel for Eiffel Programmers" tutorial. I don't see evidence of a compiler either.

(This is not a condemnation. I'm just curious if I'm missing something obvious.)

Language definiton phase

Modern Eiffel exists as a concept on my computer (i.e. a lot of textfiles which describe certain aspects of the language). I am currently writing this series of blog entries to explain the concept. This is an important step in the definiton phase, because I consider the concept as mature only if I can explain it to others. My blog is a step by step introduction to the language.

In parallel I work on the implementation of a compiler. But I won't implement anything which is not yet described in detail.

My blog has two purposes:

a) Describe the language in detail in the form of a user manual.

b) Get feedback from potential users.