/austral

Systems language with linear types and capability-based security.

Primary LanguageOCamlApache License 2.0Apache-2.0

Austral

Build status badge

Austral is a new language.

Features:

  • Linear types: linear types allow resources to be handled in a provably-safe manner. Memory can be managed safely and without runtime overhead, avoiding double free(), use-after-free errors, and double fetch errors. Other resources like file or database handles can also be handled safely.

  • Capabilities: linear capabilities enable fine-grained permissioned access to low-level facilities. Third-party dependencies can be constrained in what types of resources they can access. This makes the language less vulnerable to supply chain attacks.

  • Typeclasses: typeclasses, borrowed from Haskell, allow for bounded ad-hoc polymorphism.

  • Safe Arithmetic: Austral has well-defined semantics for all arithmetic operations on numeric types. There are distinct operations for trap-on-overflow arithmetic and modular arithmetic, as in Ada.

  • Algebraic Data Types: algebraic data types, as in ML or Haskell, with exhaustiveness checking.

Anti-features:

  • No garbage collection.
  • No destructors.
  • No exceptions (and no surprise control flow).
  • No implicit function calls.
  • No implicit type conversions.
  • No implicit copies.
  • No global state.
  • No subtyping.
  • No macros.
  • No reflection.
  • No Java-style @Annotations.
  • No type inference, type information flows in one direction.
  • No uninitialized variables.
  • No pre/post increment/decrement (x++ in C).
  • No first-class async.
  • No function overloading (except through typeclasses, where it is bounded).
  • No arithmetic precedence.
  • No variable shadowing.

Example

Calculate and print the 10th Fibonacci number:

module body Fib is
    function fib(n: Nat64): Nat64 is
        if n < 2 then
            return n;
        else
            return fib(n - 1) + fib(n - 2);
        end if;
    end;

    function main(): ExitCode is
        print("fib(10) = ");
        printLn(fib(10));
        return ExitSuccess();
    end;
end module body.

Build and run:

$ austral compile fib.aum --entrypoint=Fib:main --output=fib
$ ./fib
fib(10) = 55

Building with Nix

If you have Nix, this will be much simpler. Just:

$ nix-shell
$ make

And you're done.

Building without Nix

Building the austral compiler requires make and the dune build system for OCaml, and a C compiler for building the resulting output. You should install OCaml 4.13.0 or above.

First:

$ git clone git@github.com:austral/austral.git
$ cd austral

Next, install opam. On Debian/Ubuntu you can just do:

$ sudo apt-get install opam
$ opam init

Then, create an opam switch for austral and install dependencies via opam:

opam switch create austral 4.13.0
eval $(opam env --switch=austral)
opam install --deps-only -y .

Finally:

make

To run the tests:

$ ./run-tests.sh

To build the standard library:

$ cd standard
$ make

Usage

Suppose you have a program with modules A, B, and C, in the following files:

src/A.aui
src/A.aum

src/B.aui
src/B.aum

src/C.aui
src/C.aum

To compile this, run:

$ austral compile \
    src/A.aui,src/A.aum \
    src/B.aui,src/B.aum \
    src/C.aui,src/C.aum \
    --entrypoint=C:main \
    --output=program

The --entrypoint option must be the name of a module, followed by a colon, followed by the name of a public function with either of the following signatures:

  1. function main(): ExitCode;
  2. function main(root: RootCapability): ExitCode;

The ExitCode type has two constructors: ExitSuccess() and ExitFailure().

Finally, the --output option is just the path to dump the compiled C to.

By default, the compiler will emit C code and invoke cc automatically to produce an executable. To just produce C code, use:

$ austral compile --target-type=c [modules...] --entrypoint=Foo:main --output=program.c

If you don't need an entrypoint (because you're compiling a library), instead of --entrypoint you have to pass --no-entrypoint:

$ austral compile --target-type=c [modules...] --no-entrypoint --output=program.c

If you just want to typecheck without compiling, use the tc target type:

$ austral compile --target-type=tc [modules...]

Generated C code should be compiled with:

$ gcc -fwrapv generated.c -lm

Status

  1. The bootstrapping compiler, written in OCaml, is implemented. The main limitation is it does not support separate compilation. In practice this is not a problem: there's not enough Austral code for this to matter.

  2. The compiler implements every feature of the spec.

  3. A standard library with a few basic data structures and capability-based filesystem access is being designed.

Contributing

See: CONTRIBUTING.md

Community

Roadmap

Currently:

Near-future work:

  • Build tooling and package manager.

License

Copyright 2018–2023 Fernando Borretti.

Licensed under the Apache 2.0 license with the LLVM exception. See the LICENSE file for details.