Why not write a type system?
In grad school I was leery of type systems. Partly because I didn’t get the big deal and partly because they are gnarly to get right. One logic bug and you have a hole.
It might surprise you to know that I’ve since implemented a type system with refinement typing for a stack-based langauge.
In this post I dig into why.
A Bolt-On Type System
My initial language for working with was a FORTH clone called caternary. For a variety of reasons, stack based languages are easy to implement in Rust. What is not easy is knowing the program will work. That’s the problem a type system solves, and in FORTH it’s ridiculously easy to underflow the stack or swap arguments to a function.
What I wanted was a way to say the program was correct without any runtime dependency.
It should be possible to type check a program in CI and then run the untyped code in production and know that the fact that it type checked offline was good enough.
Perfect for an LLM
It turns out that if you only care that your type system is good-enough, and your code that you run in the type system is entirely within CI, you don’t actually need to ship a perfect type system to production. What you need is to let it co-evolve with the programs you write.
This turns out to be the perfect shape of a verification task. My FORTH-like is approximately 25k lines of code, but the trusted base that executes in production can be significantly smaller than that and can be audited by a human in an afternoon.
I contend that this form of verification is perfect for an LLM.
I shredded Robert Kleffner’s thesis on concatenative languages and implemented a spiritually similar system in Rust. Except it was all written by an LLM and I guided the property testing.
Failure Modes
The failure modes are easy and well-contained: I can type check something and have it fail to run as typed, or I can fail to type check something the runtime would accept. The former is a serious bug excluded by thorough property testing and integration testing of caternary in production. I literally don’t care that every program type checks. I care that mine does and it functions as prescribed.
Failing to type check something halts in CI.
Both failure modes are acceptable because the tested code reaches prod.
Why Type at All
Tests are like a dynamic type system, encoding behavior in a black-box fashion.
Why do we need a type system if tests are sufficient?
Because the type system offers LLMs the ability to reason about problems in FORTH code using human readable error messages. It doesn’t have to debug stack underflows or argument type mismatches.