ruby-lean is a model of the Ruby language written in Lean 4. The model is
executable: it runs Ruby programs, and every build checks its behavior against
CRuby. Because it is written in Lean, you can also prove things about what a
Ruby program does.
$ bin/ruby-lean point.rb # run a program on the model
=> 1
$ bin/ruby-lean-check point.rb # can it raise a type error?
ACCEPTED point.rb
validateD accepted this program. By validateD_safe_run, running it on the
model never ends in an uncaught NoMethodError, ArgumentError or TypeError.| You want to | Start here |
|---|---|
| Run a Ruby program on the model and compare it with CRuby | Run a program |
Show that a Sorbet-annotated program never raises NoMethodError, ArgumentError or TypeError |
Prove a program type-safe |
| Prove what a program computes, for every input | Prove a program correct |
| Read what the model says Ruby means | The semantics |
| See what has been proved and what it rests on | What is proved, What you have to trust |
| Try it without installing anything | The playground |
The project write-up explains the motivation.
You need elan (Lean), CRuby 4.0.x, uv and Python 3.12 or newer. On macOS:
curl -sSf https://elan.lean-lang.org/elan-init.sh | sh
brew install ruby python@3.12 uv
export PATH="$(brew --prefix ruby)/bin:$PATH"
make deps # the pinned gems, Sorbet among them
make prereqs # reports anything missingThen:
make run # build the model, the checker and the desugarer
echo 'puts 1 + 2' | bin/ruby-lean # 3Getting started has the details.
make checkOne command builds the model, the type checker and every proof, audits the
axioms behind each theorem, runs the checker over its corpus of typed programs,
and runs the model against CRuby over more than 1800 programs. It stops at the first
failure. Continuous integration runs the same targets on every pull request and
each one blocks the merge. make help lists the individual targets.
A first run spends most of its time compiling proofs: several minutes on a many-core machine, about half an hour on a small one. Later runs take a few minutes.
| Directory | Contents |
|---|---|
ruby-lean/RubyCore/ |
The model: an abstract machine for Ruby, and its step function stepFn |
books/ |
Every proof: facts about the model, proofs about individual programs, and the type-soundness book |
books/Books/TypeSoundness/ |
A type checker for a fragment of Sorbet-annotated Ruby, and the proof that what it accepts is safe |
desugar/ |
Ruby source to the core language the model runs |
difftest/ |
Differential testing against CRuby |
playground/ |
A browser interface: run, type-check and step through programs |
docs/ |
The documentation site (make docs-serve) |
The theorems are about the model. The model is tested against CRuby 4.0.5 on every build, and that is testing, not proof: it does not establish that the two agree on every program.
The model does not cover all of Ruby, and the type checker covers less than the model. When either meets something it does not support, it says so and stops. It does not guess. Type safety rules out three classes of exception; it does not prove termination or rule out other exceptions.
What you have to trust is the full list.
make check must pass. See Contributing.