From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <alphablock@orange.fr>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 7EF5F7FD02
	for <caml-list@sympa.inria.fr>; Sun,  3 May 2015 23:54:06 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  alphablock@orange.fr) identity=pra; client-ip=80.12.242.131;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="alphablock@orange.fr";
  x-sender="alphablock@orange.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  alphablock@orange.fr) identity=mailfrom;
  client-ip=80.12.242.131;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="alphablock@orange.fr";
  x-sender="alphablock@orange.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@smtp.smtpout.orange.fr) identity=helo;
  client-ip=80.12.242.131;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="alphablock@orange.fr";
  x-sender="postmaster@smtp.smtpout.orange.fr";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: A0CyAQDll0ZVm4PyDFBcg19cgx2wbgaTQYYIAoF9EAEBAQEBAQERAQEBAQEGCwsJIS6EIQEBBCMVUQsYAgIFIQICDwJGBg0IAogSARgJsVuNAAGFdQErgSGEdoQggQKFDIJogUUBBJYegReFKoEkgUqEWSGKZINSgQODFm2CRQEBAQ
X-IPAS-Result: A0CyAQDll0ZVm4PyDFBcg19cgx2wbgaTQYYIAoF9EAEBAQEBAQERAQEBAQEGCwsJIS6EIQEBBCMVUQsYAgIFIQICDwJGBg0IAogSARgJsVuNAAGFdQErgSGEdoQggQKFDIJogUUBBJYegReFKoEkgUqEWSGKZINSgQODFm2CRQEBAQ
X-IronPort-AV: E=Sophos;i="5.13,362,1427752800"; 
   d="scan'208";a="138750716"
Received: from smtp09.smtpout.orange.fr (HELO smtp.smtpout.orange.fr) ([80.12.242.131])
  by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 03 May 2015 23:54:06 +0200
Received: from [192.168.1.10] ([90.29.45.161])
	by mwinf5d69 with ME
	id PZu51q0063UevgA03Zu5Sp; Sun, 03 May 2015 23:54:05 +0200
X-ME-Helo: [192.168.1.10]
X-ME-Auth: YWxwaGFibG9ja0B3YW5hZG9vLmZy
X-ME-Date: Sun, 03 May 2015 23:54:05 +0200
X-ME-IP: 90.29.45.161
Message-ID: <554698FC.40409@orange.fr>
Date: Sun, 03 May 2015 23:54:04 +0200
From: Damien Guichard <alphablock@orange.fr>
User-Agent: Mozilla/5.0 (Windows NT 5.1; rv:23.0) Gecko/20100101 Firefox/23.0 SeaMonkey/2.20
MIME-Version: 1.0
To: Caml List <caml-list@inria.fr>
References: <5542B099.4070502@gmx.net>
In-Reply-To: <5542B099.4070502@gmx.net>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
X-Validation-by: alphablock@orange.fr
Subject: Re: [Caml-list] [ANN] Albatross 0.1

Congratulations.
It would be great to have yet another programming language with 
certification included.

I am quite familiar with Eiffel 3 and ECMA Eiffel.
I have quickly read the Albatross Language Description.
Your syntax is very much Eiffel-ish :)

My guess is you plan to keep inheritance (for better proof reuse) but 
sacrifice mutability.
I am right ? Can you elaborate about the final goal ?

- Damien Guichard



Helmut Brandl wrote:
> I am pleased to announce version 0.1 of the Albatross compiler.
>
> The Albatross compiler suite is written in ocaml v4.0.
>
> What is Albatross?
>
> - A programming language with static verification (allthough version 
> 0.1 is not yet able to compile real programs)
>
> - A theorem prover and a proof assistant.
>
> http://albatross-lang.sourceforge.net
>