DEV Community

Hieu Louis
Hieu Louis

Posted on Edited on

Halis 1.0.0 is out 🎉

#opensource #programming

Halis 1.0.0 is out

There's a folder on my laptop I used to open on free evenings. No repo, no plan, no users. Just something I kept poking at. At some point the poking turned into a habit, the habit turned into a repo, and the repo turned into this. Today Halis is 1.0.0 🚀

Repo: github.com/mhieuhonda/halis-lang

What is it

Halis is a systems language built around one question: what if the compiler could prove your program is safe instead of trusting you?

Systems languages usually hand you control and ask you to be careful. Careful is not a compiler guarantee. Halis moves as much of that care as it can into the type checker and the effect system, so the things you would normally catch in review or in production get caught at build time instead.

What that gives you

  • No null, no globals, no uninitialized values. If it exists, it was initialized.
  • Memory safety without a GC. Use-after-move is a compile error. Memory is freed deterministically when it leaves scope.
  • I/O is a declared effect. There are nine of them (IO, Fs, Clock, Args, Exit, Net, Rand, Proc, Conc). A function with no uses clause is pure, and the compiler verifies that across the whole call graph. You cannot sneak a file write into a helper.
  • Data races are impossible. Values cross task boundaries only through channels, and the type system enforces it.
  • Every arithmetic op is checked. Overflow, divide by zero, out of bounds. There is no off switch, not even a hidden one.
  • Untrusted input is marked tainted and cannot reach a sink until you sanitize it. Injection bugs become compile errors.
  • hlc --audit prints what every function in the program can actually do, so you can review a codebase you did not write.

A quick look 

fn greet(name: str) -> void uses IO { 
    println("Hello, " + name) 
}

fn pure_add(a: i32, b: i32) -> i32 { 
    return a + b 
}
Enter fullscreen mode Exit fullscreen mode

greet declares uses IO because it prints. pure_add has no uses clause, so the compiler guarantees it is pure. Try to call println inside it and the build fails. That is the whole idea: the guarantee is not a convention, it is a check.

Self hosting

The compiler is written in Halis. Every build proves a fixed point: from a committed C snapshot it rebuilds itself byte for byte. Bootstrap takes about 20 seconds on a normal machine. What comes out is a native binary, no interpreter, no hidden runtime underneath.

You can check this yourself:

make bootstrap
make check
Enter fullscreen mode Exit fullscreen mode

Getting started

gcc or clang and make. That's it.

git clone https://github.com/mhieuhonda/halis-lang.git
cd halis-lang
make bootstrap
make run F=examples/hello.hls
make test
Enter fullscreen mode Exit fullscreen mode

Useful extras: make audit for the capability report, make fmt for formatting, make lint for static checks.

Why 1.0.0

The language, the effect system, and the bootstrap process are settled. Not finished, settled. That means it is a good time to try it, break it, and tell me what happened. The project is still mostly me, and every issue or PR moves it forward.

If you build something with it, I want to see it. If you find a hole in one of the guarantees, I really want to see it 🙏

Repo: github.com/mhieuhonda/halis-lang

Top comments (1)

Collapse
 
vinmay profile image
Vinmay Nair •

I really like the idea of hlc --audit showing what a function can do beyond its declared capabilities. Does the audit also show the call chain responsible for each capability or just the final set of effects? I've explored reachability in one of my own projects so I'm curious how you're approaching it here.