Highly-Assured PLDI using Dependent Types.

Olaf is designed to be a proto-typical imperative language with side-effecting statements and pure expressions. We have designed the language to be purposefully minimal.

Specifically supporting:

1. primitive types and common operations on them;

2. let-binders to place values on a local stack;

3. commands to print to stdout, while-loops, conditionals, and early returns;

4. references;

5. sub-programs with methods;

Olaf does not support:

1. recursion;

2. mutually defined methods;

3. method prototypes or mutually defined methods;

4. type inference;

Primitive Types and their Constants

Olaf supports simple types:

• int :: signed integers of arbitrary size;
• bool :: boolean values of true and false;
• string :: anything within double quotation marks;
• unit :: the unit type and value unit;

Expressions

To keep things simple: Olaf supports unary and binary operations using method-call syntax.

Arithmetic operations are:

add(1,2)
mult(1,2)
div(2,0)
sub(3,5)

Boolean operations are:

and(true,true)
ior(true,false)
xor(true,false)
not(false)

Logical comparison operations on integers, booleans, and strings:

gt(1,2)
gte(1,2)
lt(1,2)
lte(1,2)
eq("1", "3")

Casting from int, bool, and string to string. As Olaf is statically typed, with no type inference¹, we require that casting to a string must explicitly state the origin type:

cast(int,1)
cast(bool,false)
cast(string,false)

Let-bindings

We can use let-bindings to create immutable variables, containing expressions, that live on a local function stack.

let x : bool = false;

Olaf is statically typed and all binders must contain the type of the expression being stored. Variables have lexical scoping, meaning that variables exist only within the context after their creation.

Variables can also be shadowed, meaning that given two binders of the same name in the same context the name refers to the latest definition.

Commands

Olaf is imperative and uses commands/statements to control program execution.

The return statement halts a method’s execution and returns the expression.

return 1;

We can print strings to STDOUT:

print "I like warm hugs, and chugging mead";"

Conditionals make decisions based on a condition, and each branch contains a further sequence (block) of statements.

if false
{
  return "1";

} else
{
  print "Warm Hugs";
}

We can iterate a inner sequence of statement whilst a boolean condition holds using while-loops:

while true
{
  print "logic bomb";
}

Aside from return statements, and like let-bindings, each statement can be sequenced together.

Memory

As well as a local stack, Olaf supports addressable memory in a stack based heap.

We place values on the heap using the var-binding statement:

var x : int = 1;

Like let-bindings, var-bindings must be typed with the value’s type.

We can deference references using the & operator:

add(&x,1)

The type of references also uses the & operator:

var x : int = 1;
let xref : &int = x;

Methods

Olaf supports methods and their syntax follows many imperative languages: We define a method prototype detailing the arguments and return type, and then the method body. Method bodies contain a sequence of statements. The last statement in a method must be the return statement.

Here is the main method that all Olaf programs must define:

fn main() -> unit
{
  return unit;
}

Here is a user-defined method that casts an integer to a string:

fn intToString( i : int) -> string
{
  return cast(int, i);
}

Method calls are expressions, here is a main method that calls intToString

fn main() -> unit
{
  print intToString(42);

  return unit;
}