RFCs

Designs for what ra-jit adds to Rust. Each one is a draft until it is not: sign in with GitHub and comment on any paragraph, or on the RFC as a whole.

Read the charter first: it says what every RFC has to keep.

• 0001 Capabilities and effects Draft
  A function's signature says what it may touch. Effects on the surface, capabilities underneath; pure code is cacheable by construction.
• 0002 Values that must be used Draft
  Types that cannot be forgotten or silently dropped, following Rust's 2026 Move/Destruct/Forget goal, in the new edition.
• 0003 Rust and Lean Draft
  Rust is the program language and Lean is the proof language. ra-jit owns the compiler, so it joins them at MIR: each function becomes a Lean definition as it compiles, and its spec becomes a theorem.
• 0004 Inferred specs Draft
  Most functions should not need a written spec. ra-jit infers one where a function meets its callers, records it by the function's content hash, and makes every change to it a visible diff.

Each RFC is a Flecs script in site/content/rfcs. To propose one, open a pull request with a new file.