Building a type-safe DSL in Rust: lessons from creating Lof

The problem

Writing zero-knowledge circuits is painful. The existing tooling forces you to think in constraints — low-level arithmetic operations that are easy to get wrong and hard to debug. I wanted a language where the type system catches constraint errors at compile time, not at proving time when you’ve already wasted 30 minutes.

That’s how Lof started: a domain-specific language that compiles to ZK circuits with static guarantees about constraint satisfaction.

The approach

The core insight was treating constraints as linear resources. In a ZK circuit, every wire must be consumed exactly once — this maps perfectly to linear types from type theory. If a constraint variable isn’t used, the type checker rejects the program.

Linear types turned out to be the bridge between type theory and ZK proof systems — something I didn’t see until both graphs connected.

The compiler pipeline is straightforward:

• Parser (hand-written recursive descent) produces an AST
• Type checker enforces linearity and constraint tracking
• IR lowering converts typed AST to constraint system
• Backend emits R1CS or Plonk constraints

The code

Here’s how the type checker tracks linear resources. Each variable gets a Usage state that the checker updates as it walks the AST:

use std::collections::HashMap;

/// Tracks how each linear variable has been used
enum Usage {
    Unused,
    Consumed,
}

struct LinearChecker {
    bindings: HashMap<String, Usage>,
}

impl LinearChecker {
    fn consume(&mut self, name: &str) -> Result<(), TypeError> {
        match self.bindings.get(name) {
            Some(Usage::Unused) => {
                self.bindings.insert(
                    name.to_string(),
                    Usage::Consumed
                );
                Ok(())
            }
            Some(Usage::Consumed) => {
                Err(TypeError::AlreadyConsumed(
                    name.to_string()
                ))
            }
            None => Err(TypeError::Unbound(
                name.to_string()
            )),
        }
    }

    /// Verify all bindings were consumed at scope end
    fn check_exhausted(&self) -> Result<(), TypeError> {
        for (name, usage) in &self.bindings {
            if matches!(usage, Usage::Unused) {
                return Err(TypeError::Unconsumed(
                    name.clone()
                ));
            }
        }
        Ok(())
    }
}

What didn’t work

My first attempt used affine types (use at most once) instead of linear types (use exactly once). This was wrong for ZK — an unused constraint variable means a missing constraint, which means the circuit is under-constrained and potentially unsound. Switching to strict linearity caught a whole class of bugs.

The other mistake was building the parser with a combinator library. It was elegant but made error messages terrible. Switching to hand-written recursive descent doubled the parser code but made error recovery actually useful.

Result

Lof compiles to R1CS constraints and catches linearity violations at compile time. The type checker adds ~2ms overhead on a 1000-constraint circuit. The constraint system output is compatible with existing ZK proving backends.

The project took over a year of development. The full source is available on GitHub.