Skip to content

Systems language with linear types and capability-based security.

License

Notifications You must be signed in to change notification settings

christos-chatzifountas-biotz-io/austral

 
 

Repository files navigation

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 [email protected]: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.

About

Systems language with linear types and capability-based security.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • OCaml 85.5%
  • TypeScript 5.5%
  • Python 3.9%
  • Standard ML 1.3%
  • C 1.1%
  • Vim Script 0.9%
  • Other 1.8%