跳到正文
DEV Community· Fujo·· 3 小時前AI 評分37

我們受夠 Rust 的借用檢查器了，是時候掙脱了

We're fed up with Rust's borrow checker. It's time to break free.

AI 導讀

Loment 在 0.1.5 加入 LSPE，為編譯器的安全決策留下可離線查閲的帳本，而非移除借用檢查。LSPE 提供 PROVED、UNDECIDED、REFUTED 三種結果；稽核開啟或關閉時，編譯決策集合相同，變化只在帳本。Loment 的借用檢查只是 Rust 的子集，不涵蓋生命週期、跨函數推理、欄位層級移動或分支敏感移動集合。

正文

I like Rust. I also dread the moment the borrow checker says no and the compiler refuses to
explain what it assumed.

That is not a complaint about competence. Rust's borrow checker is one of the most valuable
things to happen to systems programming. It is a complaint about posture: the compiler stands
outside your program, announces a verdict, and the burden of proof lands on you. When the verdict
is wrong, there is often no receipt to inspect.

We built Loment around a different posture. It keeps the
checks; it moves the burden. This post is about what that means precisely, because "we removed the
borrow checker" would be a lie, and the interesting part is not the removal.

What Loment keeps

Loment is a systems language with a Rust-flavoured surface. It still checks the ownership
mistakes that matter most:

  • use after move (E006),
  • a mutable borrow alongside another borrow (E007),
  • a dangling reference (E012).

It also adds capability domains (capability disk[0..4] plus guard), compiles to a native
ELF/PE artifact with no runtime by default, and has two implementations — a Python reference and
a self-hosted one — that must emit byte-identical IR.

What it does not do is pretend to be Rust's borrow checker. The boundary is written down in
the repository: it proves three things and explicitly does not prove four others (no lifetimes, no
cross-function reasoning, no field-level moves, no branch-sensitive move sets). Keep that in mind
for the rest of this post.

From verdict to receipt

The change is a seventh choose dimension called LSPE — Loment Safety Police Espace. It does
not change any verdict. It changes what a verdict leaves behind.

With lspe_open_admin (the default), every allowance is recorded in the artifact's Potato v16
ledger: the site, the obligation, the evidence, and what is still unproved. With
lspe_close_admin, the recording is turned off; the LMS, runtime and capability decisions are
unchanged. The audit is not a second checker bolted on top — it is a ledger of the compiler's own
decisions, answerable offline.

The design document puts it more bluntly than I can:

Rust's borrow checker is a god. LSPE is a shop assistant.

A god stands outside the transaction and says "no". An assistant stands inside it, has to name the
price, and gives you a receipt. Concretely, LSPE has three outcomes instead of two:

  • PROVED — here is the evidence;
  • UNDECIDED — here is the site where my proof has a hole;
  • REFUTED — here is a counterexample, so this is a hard no.

"Undecided" is a first-class result. In strict mode it becomes E034; the ledger's own consistency
failures are E035–E037. The point is not that the compiler is always right. The point is that when
it is wrong, you can point at the site and the obligation instead of arguing with a verdict.

"Gentle" is a measurable claim

It is easy to say a checker is friendlier. We tried to make it falsifiable:

  1. Same verdicts. Compile the same corpus with the audit open and closed: the set of decisions is identical. The audit changes the ledger, not the language.
  2. No silent permit. Every allow has a source, or an explicitly recorded assumption. An allow with neither is an error in the ledger.
  3. No overclaiming. LSPE does not claim to prove more than Rust. What it adds is accountability, not completeness. The remaining cases are UNDECIDED and labeled.

That is the sense in which it is "gentler with nearly the same safety": not that it catches
everything Rust catches, but that the same checks no longer arrive as an unaccountable verdict.

Loment also has a memory-safety ladder, lms, with seven levels and four tiers
(lms_full, lms_forensic_admin, lms_daily_admin, lms_manage_only_admin). The default is
full; writing a lower tier is a downgrade and carries _admin. The literal-out-of-range check is
E028; use-after-free is E029.

What it looks like

The defaults, written out:

module demo
choose runtime
choose lms_full
choose lspe_open_admin

capability disk_slots : disk[0..4] revocable

fn write_slot(slot: u32) -> u32 {
    guard disk_slots(slot);
    return slot;
}

fn _start() {
    let xs: [u32; 3] = [1, 2, 3];
    let i: u32 = 5;
    if i < 3 {
        xs[i] = 7;          // a runtime index: you guard it, the language does not guess
    }
    syscall4(60, 0, 0, 0);
}

Two details matter here. guard bounds the index, not the subject — it is not authorization.
And the array write is still your responsibility: Loment refuses a literal out-of-range index
at compile time (E028), but a runtime index is not silently checked.

What this does not mean

I would rather say this before the comments do:

  • Loment is early. 0.1.5 is the release where LSPE lands; the packaged front end is still being finished. Do not rewrite your service in it this weekend.
  • It is not Rust. The borrow checking is a subset. No lifetimes, no cross-function reasoning, no field-level moves, no branch-sensitive move sets.
  • "No receipt" is not the same as "no bug". LSPE records the compiler's decisions; it does not make the compiler omniscient.
  • Defaults are not free. lms_full is the default and it changes the emitted artifact (inline bounds checks on alloc(<const>)-derived accesses). That exception is documented, not hidden.
  • The benchmark is a pilot. We measured an LLM agent writing Loment from the guide alone: three tasks, one attempt each, Rust and Python as controls. It is a direction, not a confidence interval.

The reason I care about the receipt is not abstract. Rust's own tracker has a soundness bug
(#164250) where an obligation was not rechecked after substitution, and it stayed invisible for
years — not because Rust's team is careless, but because a verdict-only compiler leaves nothing
to audit when the verdict is wrong. LSPE's answer to that shape is a record with a site id
(Q004 stale_wf), readable offline. That is the part I want other language designers to steal,
whether or not they like Loment.

Try it, then tell us where the receipt is wrong

We are not asking you to believe the slogan. We are asking you to compile something, read the
ledger, and tell us which line is wrong. That is the whole point of moving the burden.

Disclosure: I'm one of Loment's authors. This draft was prepared with an AI assistant and
reviewed before publishing.

來源：DEV Community · dev.to

#教學/實踐#編碼