# The ÆON programming language

Test, *Test*, 1900

**Æon** is a programming language with polymorphism and non-restricted-refined types. This language is used as the basis for Refinement Typed Genetic Programming due to its support of static verification of polymorphism. It is important to make notice that while the **Æon** language does not make any distiction, there are two classes of refinements: **liquid refinements** and **non-liquid refinements**.

**Liquid refinements** are those whose satisfiability is statically verified using a SMT Solver.

**Non-Liquid refinements** are those that SMT solvers are not able to reason about, thus being checked at runtime.

## Libraries

To more easily allow the interaction of the user with the language, **Æon** provides different kinds of implemented **libraries**. The specification of each function for each library can be found in the **proper markdown**.

## Examples

**Æon** acts like syntactic sugar from its core, providing a user friendly syntax, making it easy and intuitive for a new user to engage into program synthesis. The following examples present the basics of the language, many more can be found in the **examples** folder.

We start by defining a new **Nat** type by refining the **Integer** type with the condition *x >= 0*. The program computes the fibonacci from a given value with type **Nat**. The output of the functions is restrictively refined to ensure that we never compute a value smaller or equal than the input. The body of the function is implemented using the inline **if then else** expression.

```
type Nat as {x:Integer | x >= 0};
fibonacci(x:Nat) -> {y:Nat | y >= x} {
if (x <= 1) then x else (n - 1) + fibonacci(n - 2);
}
```

Similarly to the previous example, we create a type alias **RestrictedValue** by refining the **Integer** type. **Æon** allows low-level details to be implemented in another language by using the **native** construct. The *buildKey* and *getKey* functions are natively implemented in the language. The **decipher** function takes an integer and deciphers the value with the key. The output function ensures that our implementation is bug free! In this case a type exception would raise since the *i* variable can take any value even smaller than `k.key`

. One could easily fix this by refining key value to ensure that it is smaller than *i*, `{k:Key | k.key < < i}`

. In the **cipher** function by providing the hole operator, `??`

, we are able to delegate the implementation of the function to the compiler. We present our intention of the function behaviour with the **where** specification, in a way to help the synthesis of the program.

```
type RestrictedValue as {x:Integer | x >= 0 && x <= 1024};
type Key {
{key : RestrictedValue};
}
buildKey(i:RestrictedValue) -> {k:Key | k.key == i} = native;
getKey(key:Key) -> key:RestrictedValue = native;
decipher(i:Integer, k:Key) -> {j:Integer | j > 0} {
i - getKey(k);
}
cipher(i:Integer, k:Key) -> j:Integer where {j >= 0 and i == decipher(j, getKey(k))} {
??;
}
```