Saber

Saber is a project creating three tools currently under development, and can be thought of as a programming language. The tools are:

• The Saber Programming Language, or Saber

• The Saber Proof Assistant, or SaberPA

• The Saber Virtual Machine, or SaberVM

SaberPA

The project with the most progress is SaberPA. It uses a Cedille-inspired dependent type theory for proving theorems. It is still broken in very critical ways (type checker conversion checking) but an MVP is mostly done. Like Cedille, it will be able to express many interesting mathematical theorems. Unlike Cedille, it superficially look and feel similar to Saber code, including using functions with multiple parameters and literals that aren't lambda encodings, and it will exist primarly for writing machine-checked proofs about code written in Saber, which programmers can use to get around some of the limitations of Saber's type checker, as well as optimize code with equalities.

The long term goal for SaberPA is to include a coeffect system for reflecting resource management, which I might implement directly since I assume CDLE can internalize it, but I might add it (in an admissable way) to make SaberPA code easier to write. I'm quite confident that Saber will have a coeffect system so it would be nice for the two to interact cleanly.

The choice of Cedille's type theory (CDLE) comes from a few reasons, the main two being 1) the Curry-style typing means terms from Saber can be given more informative types in a subtype relation, and 2) the simplicity of CDLE makes SaberPA much easier to implement, and to port across systems.

SaberPA is written in Gleam, a statically typed scripting language for the BEAM, though I'm using a javascript-based runtime for it instead. I may port to a faster language in the future (likely Saber itself) but currently have no reason to, and I'm very very productive in Gleam.

The name of this proof assistant is subject to change.

SaberVM

The next furthest along, and the far more interesting project overall, is SaberVM. SaberVM is intended to be a general bytecode language for functional languages, so when it's completed you should consider targeting it for your language! It's intended to fill a gap of functional compiler backends because LLVM does CPS poorly. However, SaberVM has a quite opinionated design. The bytecode language is a typed stack-based assembly language, like Web Assembly, but it's designed to be:

• Easier to implement your own verifier and VM on any platform

• AOT-compilation oriented, for resource-constrained environments

• Optionally memory safe and information secure, with a combination of coeffect-based static analysis and dynamic runtime checks

• Very fast when safety is turned off and the bytecode is AOT compiled, in which case SaberVM is like LLVM for functional languages. This doesn't clash with the first point, since different SaberVM implementations can perform different amounts of optimization, and need not AOT compile either.

• Robust in a crash-only-software way, like Erlang's BEAM backend, even when AOT compiled

• Planned around parallel execution from the get-go

• Immutable by default, and offering the traditional optimizations for functional languages

Currently, the bytecode language is still being designed, though the design is easily about 90% completed. I expect it to be straightforward to implement, which is a design goal. Much of the design is stolen from Greg Morrisett's wonderful research into typed assembly language and static memory safety; research that had a huge impact on the design of Rust. Hopefully, functional languages will be able to produce SaberVM bytecode, which can be passed to clients that can trustlessly AOT compile it and run it on their own machines. 

It's intended to be fast and flexible. Garbage collectors can be written for it, or not, it supports unboxed data or not, it supports mutable reference types as well as immutability-based optimizations, linearity-based in-place mutation optimizations without using mutable reference types, etc. Safety thus often means runtime checks, including memory accesses, so SaberVM uses a built-in notion of panic which allows the program to keep running when parts of it cause a crash, and thus microrebooting those parts or crashing other parts, etc. This is very Erlang-inspired. In the mode with safety turned off, the same bytecode doesn't cause those runtime checks to happen, which means these crashes are more or less only caused by runtime memory exceptions, but in those cases the same panic architecture still catches the exception and takes over.

Saber

Lastly, there's the language itself, which ironically has the least progress so far. Saber compiles to SaberVM and works with the Saber Proof Assistant, unsurprisingly. The design is simply to surface many of the features of SaberVM to the high-level functional language user. The type system is a full System F-omega, which can import proved assertions and equalities from SaberPA axiomatically. If SaberVM needs static information about terms that Saber can't give it (like if a term is polymorphic) then runtime information is passed around to switch on at runtime, like the language Sixten. A coeffect system based on capabilities manages varying levels of function purity and information security.