Home » forums » LtU Forum

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.

By hbrandl at 2012-03-08 20:32 | LtU Forum | previous forum topic | next forum topic | other blogs | 4177 reads

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.)

By John Nowak at Fri, 2012-03-09 14:09 | login or register to post comments

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.

By hbrandl at Fri, 2012-03-09 14:54 | login or register to post comments