Statically verified: Each program has a specification and the proof engine verifies that the program satisfies its specification.
Functional, imperative and concurrent: Albatross combines the power of functional, imperative and concurrent languages
Like in your favorite functional language it is possible to use inductive/algebraic data types and to write recursive functions with pattern matching.
Imperative elements like arrays with random access, mutable data structures, flow control constructs like loops, alternative statements etc. are available in Albatross. In principle it is possible to write a certified operating system in Albatross.
Concurrency is supported by processes. Any Albatross program is a process which interacts with its environment by reading and writing to files, listening and responding to sockets. Internally an Albatross program can split up the work to various concurrently executing processes.
use alba.base.boolean end all (a:BOOLEAN) require a ensure a end