It is my pleasure to announce a new version of the compiler for the Albatross programming language. It is available via ‘opam install alba’ (it requires ocaml >= 4.03.0).
Alba is a language which allows static verification. In its current state it supports inductive types, recursive functions, pattern matching, inductively defined sets and relations and abstract data types. It can be used like coq to define types and functions and prove properties about them. We claim that Albatross is easier to use than coq and closer to mainstream languages so that there is no steep learning curve.
The design of the language is an ongoing activity. Any comments, hints, issue reports etc. are welcome. Its long term goal is to open software verification for the masses.