Home » forums » LtU Forum

Albatross has grown two mighty wings: Induction and Recursion

The version 0.2 of the Albatross programming language / proof assistant has been released.

It has some new features. The most important ones are induction and recursion which come together with inductive data types. With these two features Albatross approaches the expressiveness of Coq. It is possible to declare lists, trees, define recursive functions on them and prove properties of these functions.

The documentation contains examples of lists, binary trees and a verified insertion sort algorithm. All the examples a fully verifiable with the version 0.2 of the Albatross compiler (download here).

Some of the key features of Albatross:

  • No special proof language: All proofs are expressed via boolean expressions. Like a mathematician you make assumptions a draw step by step conclusions
  • Defined and understandable proof automation: There are no tactics. Everybody who understands the language and its proof engine can understand proofs without executing them. Proofs communicate to the human reader and to the compiler
  • Albatross' logic is classical predicate logic which is easier to understand for those not familiar with dependant type theory.
  • Albatross has been designed from the beginning as a programming language. I.e. once the backend is available, Albatross programs can be compiled to executable code without any intermediate code extraction.
By hbrandl at 2015-08-05 18:56 | LtU Forum | previous forum topic | next forum topic | other blogs | 3177 reads

Comment viewing options

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

pragmatics

I think this is cool. The more the merrier when it comes to people making formal methods more available and accessible. Some pragmatic questions: I had to dig around to find out it uses Ocaml. I assume that means it works anywhere Ocaml works? Is there a story for FFI yet?

By raould at Wed, 2015-08-05 23:09 | login or register to post comments

Your questions:

1. The Albatross compiler is written in Ocaml. Therefore you need the Ocaml compiler to compile the Albatross compiler. After compiling the Albatross compiler you don't need Ocaml anymore. Binary distributions of the Albatross compiler will be available as soon as I find someone who helps me for Windows and someone for MacOS. Having binary distributions there is no need for the Ocaml compiler anymore.

2. FFI: There are some ideas, but not yet a story. But definitely a foreign function interface is necessary. This belongs to the backend of the compiler which is not yet implemented.

By hbrandl at Sun, 2015-08-09 00:55 | login or register to post comments