Provably Safe System Programming

Recently I’ve tried to find a safer way to write software than using Rust. There are two approaches: dependent types, and language-supported algebraic effects.

By the way, I think a language should support three kinds of primitives:

• Nat/Int (beta reduction)
• List (singly linked list -> flat buffer)
• Stackable Monads (erased at run time)

All the languages this articles have either type that depend on term, or have algebraic effects (or planned). Neither of them require manual memory management (they use copy by value semantic).

Anyway, here’s the code.

F*

F Star is in the ML family, but with dependent types. It compiles to OCaml. Personally, it’s too verbose for me.

Hello.fst:

module Hello

open FStar.HyperStack.ST
open LowStar.Printf

val main : unit -> St unit
let main () =
    let a = 1 in
    print_string "hello";
    print_string (Printf.sprintf "Hello %d\n" a);
    ()

build script:

fstar --extract Hello --codegen OCaml --odir out Hello.fst
ocamlbuild -pkg batteries -pkg fstarlib out/Hello.native

It also has a subset (Low*), which compiles to simple C. You can’t use the I/O part of F* standard library if you plan to compile to C, since it is only written in OCaml.

Bring your own native libraries! All the languages in this articles don’t have much ecosystems. You should be able to use C/Zig libraries quite easily with them though.

Lean Prover 4

Lean Prover is a language associated with Microsoft. It has the best syntax of all the compile-time type checked languages I tried.

It generates POSIX C, which you need Emscripten to compile to WASM/JS.

BTW, When I say “POSIX C” is this article, I mean the generated binary depends on POSIX API that can’t be easily ported to WASM. I tried to compile every single language to WASM with Zig, but they are too heavily coupled with POSIX API.

Hello.lean:

def hello := "world"

compile:

lean -c Hello.c Hello.lean
leanc -o Hello Hello.c

leanc is just a clang wrapper script. You should can use Zig for this.

Idris 2

Idris is the language made for academic use. However, it has a refc backend that compiles the code to POSIX C. The FFI is a bit confusing, and it also can’t create static/shared native libraries. If you want to create a native library, you need to use the output C code and C compiler to do it yourself (omitted due to scope of this article).

hello.idr:

main : IO ()
main = putStrLn "Hello"

compile: idris2 --cg refc -o hello hello.idr

Note that the executable is created at build/exec/hello.

Koka

A language by the creators of Lean (also from Microsoft). The runtime is also tied to POSIX systems.

I think it is the first language implementing algebraic effects. If not for the papers by its authors, my language (algograph) would not exist.

Currently it’s under a heavy rewrite, so the official documentation lagged behind. I recommend checking this a year later.

Ante

An interesting language that use Cranelift/LLVM. It doesn’t have dependent types. Algebraic effects is only planned.

It has a good syntax, and the cleanest codegen output I’ve seen.

hello.an:

print "Hello, World!"

compile to WASM:

ante -eir --backend llvm hello.an > hello.ll
zig cc --target=wasm32-wasi hello.ll
wasmtime a.out

I actually succeed building this to WASM on first try with Zig! Try using Zig as a C/LLVM IR compiler yourself!

Neut

I had no idea what I was looking, and I still have no idea. Don’t read any documentation, since it’s all out-dated. Read this instead.

It seems to compile to LLVM IR as well. It’s still too early to be used though, I think. Maybe a year later.

That’s all. Wish you code with less pain.

P.S. On a tangent note, Futhark compiles to C/OpenCL/CUDA that makes your code go brrrrrrrrr.