DEV Community

wintrover
wintrover

Posted on • Originally published at wintrover.github.io

Nim vs Rust: Language is a Matter of 'Coherence', Not 'Performance'

#axiom #nim #formal #verification

I once spent a long time debating between two languages as the foundation for a formal verification engine.
One was Rust, bringing its borrow checker and lifetimes. The other was Nim, leading with func and distinct.

When people compare these two, the conversation usually boils down to "Rust's memory safety vs. Nim's C-compatibility and productivity."
But when you actually try to build something like the Axiom proof engine from the ground up, the real wall you hit is entirely different.

Especially in an environment where AI generates code, the most terrifying bottleneck isn't a 'compile error'—it's 'semantic opacity'.
LLMs can easily spit out code that flawlessly passes tests while subtly twisting the author's original intent into something unrecognizable.

There is No Perfect Symmetry: The Trade-off Between Memory and Intent

"Rust prevents memory corruption, while Nim prevents intent corruption."
Saying it like that sounds incredibly clean and punchy, but real-world engineering is rarely that neat.

Of course, Rust is perfectly capable of expressing semantics. You can use the Typestate pattern or the Newtype pattern to rigorously enforce domain meaning. It's not that Rust can't express intent. The issue is the cognitive cost required to express that intent.

Conversely, Nim is not a silver bullet. Debugging complex macros can sometimes feel like hell, and the smaller ecosystem can be a real pressure point. This is a clear trade-off.

However, the reason I accepted this trade-off and sided with Nim comes down to how we distribute our 'attention' when collaborating with AI.

Syntactic Simplicity: Where Does Our Attention Go?

When reviewing code generated by an LLM, our cognitive resources are strictly limited.

Let's look at Rust:

fn explore<'a>(
    step: usize,
    trace: &'a BmcTrace,
    verdict: BmcVerdict,
    rule: &'a TransitionRule,
) -> BmcVerdict {
Enter fullscreen mode Exit fullscreen mode

When I read this code, a massive chunk of my brainpower is spent tracking lifetimes ('a), references, and mutability.
In fact, when a bug occurred here, I found it incredibly difficult to tell at a glance: is the domain logic wrong, or was this code just awkwardly structured to appease the borrow checker?

Now, how about Nim?

func explore(step: int; trace: BmcTrace;
             verdict: BmcVerdict;
             rule: TransitionRule): BmcVerdict {.raises: [].} =
Enter fullscreen mode Exit fullscreen mode

Here, my attention is entirely focused on the 'domain variables' and 'semantic constraints'.
Because the concerns of memory management are stripped away from the syntax, I can focus on the causality of the logic itself, rather than the grammar.

Structural Devices That Enforce the "Why"

The most painful moments in the trenches are when you have to dig through comments or commit messages to figure out "why did the previous dev (or yesterday's me, or the LLM) write it this way?"

Nim allows you to bake this 'Why' directly into the language spec.

type
  SessionId = distinct string
  OwnerId = distinct string
Enter fullscreen mode Exit fullscreen mode

distinct is not just a type alias. If an AI makes the mistake of passing an OwnerId where a SessionId is expected, the compiler grabs it by the collar immediately—long before it ever reaches runtime tests.

The same goes for contracts that specify the preconditions and guaranteed outcomes of a function:

func toSessionId*(raw: string): Result[SessionId, AxiomError] {.
  raises: [],
  requires: raw.len > 0,
  ensures: (not result.isOk()) or
           (sessionIdString(result.get()) == raw)
.}
Enter fullscreen mode Exit fullscreen mode

This isn't mere documentation. It's a contract enforced by the compiler before runtime.
Sure, you can mimic this in Rust using macros or external crates, but Nim's core philosophy pushes this 'visibility of intent' by default. Just like how the single func keyword structurally enforces the absence of side effects at the module level.

Conclusion: The Real Bottleneck in the AI Era

To reiterate, if performance or the sheer size of the community is your primary concern, Rust is undoubtedly an excellent choice. It provides an incredibly solid floor of memory safety.

But what I felt in my bones while building Axiom is that, in the era of AI-assisted development, the most terrifying risk isn't 'unsafe code'. It's 'code where you cannot know what it intended until you run it.'

Can you structurally grasp the author's intent without having to read every line of code?
I didn't want to compromise on this question. And that—even if it sometimes looks a bit rough around the edges—is why I chose Nim. To break through the ceiling of coherence.

Top comments (0)