Home » forums » LtU Forum

Albatross formerly called Modern Eiffel is available

Some of you might have followed some of my posts during 2012/2013 where I described the design of a programming language which allows static verification.

The previous working title had been "Modern Eiffel" since my first attempt had been to create a variant of Eiffel which allows static verification. During the language design more and more weaknesses of Eiffel popped up which are in the way to do static verification. The most prominent weak point is that Classical Eiffel is not type safe.

The result of my language design activities is a new language which has some syntactic resemblance to Eiffel.

However semantically the new language now called Albatross is more like Coq or Isabelle because it has a functional core and it allows to state assertions and prove them.

The last to years I have worked on a compiler and verifier for the language. The effort clearly has been underestimated by me and the one-year project has already taken two years and the available implementation has still a lot of restrictions. However the theorem prover works quite well and it certainly will take some time to complete the compiler.

For those of you who know Coq you might enjoy the capabilities of the proof engine and enjoy the fact that there is no extra proof language and all proofs are expressed by pure statements in predicate logic. Proof automation is done by predicate calculus as well and no by an integrated language like Ltac. Therefore the language is easier to learn than Coq, because every programmer has a well developed intuition about logic.

You can find the downloadable version of the compiler and a language description at the Albatross website.

By hbrandl at 2015-05-01 00:42 | LtU Forum | previous forum topic | next forum topic | other blogs | 4945 reads

Comment viewing options

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

congratulations

Happy your project is moving along. It is great to see other things that say, "the ability to prove is good". :-)

By raould at Fri, 2015-05-01 18:11 | login or register to post comments

Thanks for your interest in

Thanks for your interest in my project.

By hbrandl at Tue, 2015-05-05 23:07 | login or register to post comments

Congrats on the release

I've always thought your posts here were interesting. I don't you think you intended wordplay, but I initially read your subject line as "My personal burden formerly called Modern Eiffel is available".

By Matt M at Wed, 2015-05-06 01:09 | login or register to post comments

Why do you read "My personal

Why do you read "My personal burden ..."?

By hbrandl at Wed, 2015-05-06 08:08 | login or register to post comments

Albatross other meaning

There is an Albatross_(metaphor) Wikipedia page.

By Matt M at Wed, 2015-05-06 12:18 | login or register to post comments

Uiih. I had not been aware

Uiih. I had not been aware of this negative connotation.

Should I reconsider the name?

By hbrandl at Wed, 2015-05-06 17:51 | login or register to post comments

what you make of it

Seems to me the significance of the name is what you make of it. As the article notes, an albatross is a good omen; the mariner in the rime curses himself by killing it (and thus rejecting the good omen). And, of course, an albatross in golf is a hole three under par (one better than an eagle).

By John Shutt at Wed, 2015-05-06 18:38 | login or register to post comments

Possibly

There is this:
https://www.youtube.com/watch?v=Z_u7VGiMO0U
It's not attractive there either.

By Josh Scholar at Wed, 2015-05-06 21:33 | login or register to post comments

What precedence would you propose for boolean negation?

For Albatross I have used most of the operator precedences of Eiffel. Most of them seem quite natural. But I am beginning to dislike the precedence for boolean negation and would like to get some opinions. Currently negation has a higher precedence than relational operators and arithmetic operators which forces you to use parentheses like not (a <= b), not (a = b + x).

But since not a doesn't make any sense unless a is of boolean type I have the tendency to drop the parentheses and write

not a <= b
not a = b + x

i.e. giving the boolean negation operator a lower precedence than relational and arithmetic operators (but still giving it a higher precedence than all other boolean operators).

What is your opinion? I know it is a matter of taste but sometimes taste matters.

By hbrandl at Wed, 2015-05-06 13:59 | login or register to post comments

That's what python does

So it's probably a reasonable choice.

By Matt M at Wed, 2015-05-06 14:50 | login or register to post comments

Is (not) a function?

It is not clear to me that (not) is a special operator compared to other functions: I would expect it to use the same usage syntax (and precedence) as other function calls in your language syntax -- which seems to be f(a) in your case.

Fun fact: the argument that "(not) applies to boolean therefore (not a = b) makes sense with not(a = b) rather than not(a) = b" does not hold when a, b are booleans, yet when a, b are booleans, *but*:

- "not (a = b)" and "not(a) = b" are equivalent
- "not (a /= b)" and "not(a) /= b" are equivalent
- but this does not work for (<), (<=), (>) or (>=)

By gasche at Wed, 2015-05-06 15:06 | login or register to post comments

Also holds in python


if not False >= False:
    print 'nope'
if (not False) >= False:
    print 'yep'

This doesn't bother me like some other aspects of python (scoping, def clobbering, ...)

Fun fact: <= is implication on booleans but the arrow points the wrong way.

By Matt M at Wed, 2015-05-06 15:41 | login or register to post comments

not is a unary operator.

not is a unary operator. Therefore not a is the negation of the boolean a. Clearly you can write extra parentheses like not (a), but these are unnecessary and not related to the precedence of the not operator.

I was asking for opinions on the precedence of the negation operator. To make my question clearer I use in the following three coloumns. The first is the expression in source code. The second and the third are two different possibilities to parse the expression:

source code        interpretation 1     interpretation 2
not a = b          (not a) = b          not (a = b)
not a <=b          (not a) <= b         not (a <= b)
not a = b + x      (not a) = b + x      not (a = b + x)

The first alternative follows the original precedence in Eiffel and the precedence of the ! operator in the C family of programming languages.

My tendency is to use the second interpretation and if I have understood the comments on this post correctly then some of you would prefer the second interpretation as well.

By hbrandl at Fri, 2015-05-08 19:57 | login or register to post comments