All Projects → austral → austral

austral / austral

Licence: Apache-2.0 license
Systems language with linear types and capability-based security.

Programming Languages

ocaml
1615 projects
python
139335 projects - #7 most used programming language
Standard ML
205 projects
c
50402 projects - #5 most used programming language
Vim Script
2826 projects
emacs lisp
2029 projects

Projects that are alternatives of or similar to austral

newspeak
Newspeak is a live object-capability language in the Smalltalk tradition
Stars: ✭ 73 (-87.67%)
Mutual labels:  capabilities
libcap-ng
Libcap-ng is a library for Linux that makes using posix capabilities easy.
Stars: ✭ 37 (-93.75%)
Mutual labels:  capabilities
rest-api-endpoints
🌾 WordPress REST API endpoints
Stars: ✭ 31 (-94.76%)
Mutual labels:  capabilities
cap9
Capability-based security protocol for smart contracts
Stars: ✭ 22 (-96.28%)
Mutual labels:  capabilities
potd
A high scalable low to medium interactive SSH/TCP honeypot using Linux Namespaces, capabilities, seccomp, cgroups designed for OpenWrt and IoT devices.
Stars: ✭ 28 (-95.27%)
Mutual labels:  capabilities
rchain-api
An API for rchain dapps to communicate with the blockchain
Stars: ✭ 22 (-96.28%)
Mutual labels:  capabilities
view-admin-as
View the WordPress admin as a different role, switch between users, temporarily change your capabilities, set default screen settings for roles, manage your roles and capabilities.
Stars: ✭ 44 (-92.57%)
Mutual labels:  capabilities
vesper
Single-address-space capability-based nanokernel
Stars: ✭ 55 (-90.71%)
Mutual labels:  capabilities
go-traits
A concept package that helps implement mixin behavior using embedded structs and hook interfaces.
Stars: ✭ 21 (-96.45%)
Mutual labels:  capabilities
NumLin
NumLin: Linear Types for Linear Algebra
Stars: ✭ 21 (-96.45%)
Mutual labels:  linear-types
juvix
Juvix empowers developers to write code in a high-level, functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment and execution.
Stars: ✭ 301 (-49.16%)
Mutual labels:  linear-types
flow-ft
The Fungible Token standard on the Flow Blockchain
Stars: ✭ 120 (-79.73%)
Mutual labels:  linear-types
linear-scala
Linear types in Scala
Stars: ✭ 28 (-95.27%)
Mutual labels:  linear-types

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 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

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, install opam. On Debian/Ubuntu you can just do:

$ sudo apt-get install opam
$ opam init
$ opam install dune

Then:

$ git clone [email protected]:austral/austral.git
$ cd austral
$ ./install-ocaml-deps.sh
$ make

To run the tests:

$ ./run-tests.sh

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.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].