Anzen is a general-purpose programming language that aims at bridging the gap between modern programming and software verification.

The goal of the Anzen is to offer a modern approach to programming, through the support of several paradigms, while also embedding a comprehensive built-in support for static (a.k.a. compile-time) and dynamic (a.k.a. run-time) checks. The language comes with a powerful program checker that uses the code itself as a model to detect errors and design test scenarios.

Why Anzen?

Anzen aims at being as accessible as popular modern scripting languages:

let attributes <- [ "simple", "concise", "safe" ]
for let attr in attributes {
  print("Anzen is " + attr)

Anzen does not need overly verbose type annotations, yet it is equipped with a powerful built-in support for complex static constraint verification, such as:

Type safety Code should clearly express the programmer’s intention, and should always behave accordingly, leaving no place for undefined behavior. This is why Anzen places a strong emphasis on types, making sure variables always hold values of the type they are supposed to.

var x <- 42
// error: cannot assign a r-value of type 'String' to a l-value of type 'Int'
x <- "foo"

Memory safety Type safety is often insufficient to guarantee the correctness of a code, as one as also to make sure memory is properly initialized, accessed and freed. Anzen features a powerful memory model that can make guarantees on safe memory operations.

let fruits: @mut <- [ "apple", "orange", "peach" ]
for fruit in fruits {
  // error: cannot call mutating method 'remove' on reference borrowed immutable
  fruits.remove(at <- fruits.index(of &- fruit))

Semantic conformance While Java-like interfaces allows for syntactical conformance to be expressed, Anzen also supports the definition of semantic interfaces to describe semantic constraints.

interface OrderedCollection refines Collection
    Element is Comparable
    forall x: Self.Index, forall y: Self.Index,
      (x < y) implies (self[x] <= self[y])
  get min: Element { return self[self.first_index] }
  get max: Element { return self[self.last_index] }

Check out the section about Safety for more information about what Anzen can offer.