spec
The shape of the data: families and signatures, what a program is about. Uses are not counted, and recursion does not have to shrink. Nothing here is compiled.
emit · omit
a language for programs you can prove
Prove real programs correct. Then run them.
You write the program and the proof in one file. The checker accepts both, or neither. What runs is ordinary Elixir. The proof is checked, then gone.
Scroll the wallmuro, n. · wall
A type is not a proof. A proof is not a program.
Muro is Spanish for wall. A specification, a theorem, and a program are three different things, and nothing is promoted from one to the next. That separation is the language. It is proved for the core of the calculus, and the checker you run is proved to follow it.
three kinds of definition
You say which one you are writing.
A program may call other programs, and a proof may talk about a program. A type stays a type. The checker refuses the other way.
evidence
The theorem, written like any other term: match, rewrite, refl. Held to the same standard as a program, then erased. Passing a value to a theorem does not spend that value.
emit · omit
run
The program. It must shrink when it calls itself, and each
variable is used at most once unless you mark plain data
reusable. This becomes an Elixir function. run internal
is the private one, a defp.
emit · Elixir def
A cell is yes when the row may appear in the column
| run | evidence | spec | |
|---|---|---|---|
| run | yes | yes | yes |
| evidence | no | yes | yes |
| spec | no | no | yes |
what you get
Nothing is guessed.
Every type is written. Every step of a proof is written. There are no holes and no tactics. If the checker says yes, that yes is a derivation.
Each value, once
A variable in a program or a proof is used at most once.
Numbers, lists, and other plain data can be marked reusable.
A pair is opened once and gives you both pieces: let (a, b) = e in t.
Taking the first and the second separately would use it twice.
Recursion shrinks
A self-call must pass a smaller value, on one argument, the same argument every time. The checker finds which one. A loop that does not shrink is refused, including a loop hidden inside another function.
Equations do not run
{a ≡ b : A}
holds when both sides compute to the same term. A rewrite
names the goal it changes. The equation is checked.
It is not in the code that runs.
If it checks, it holds
The checker is proved to agree with the judgment, for functions, data, pairs, and equality. Acceptance is a derivation. Running out of fuel is an error you raise and retry, not a quiet yes. Streams and indexed matches sit outside that proof.
A type is not a proof. A proof is not a program.
the example
half of eight is four.
Evenness is a type. half is a program. The proof
that half of an even number, taken twice, is the number, is
a third definition. It is an ordinary term. It is not emitted.
4 half of eight
-- a type is not a proof
-- a proof is not a program
def IsEven : spec Π (n : Nat) → Type := …
def half : run Π (n : Nat) → Nat := …
def half_ok : evidence
Π (n : Nat) → Π (e : IsEven n) →
{plus (half n) (half n) ≡ n : Nat} := …who checks what
Mix checks the file. Agda proves the language.
Elixir parses .muro, checks it, and emits the program.
That is the only check a file gets. Agda does not read your program
and does not take part in the verdict.
Elixir
The checker you run. A public definition becomes def,
a private one defp. A proof is omitted. One that
slipped through would be raise "erased term", not
a function.
Agda
The proof of Muro itself: the rules, the wall, and the theorem
that the checker follows them on the fragment. A few examples
are written a second time in Agda, beside the .muro
file, so the two can be compared. That copy is not a check.
Prove the program. Then run the program.
try it
Check a file.
Write a .muro
program. mix muro.check
is the whole interface.
Agda is how the language is proved. It is not installed to write one.
$ git clone https://github.com/murolang/muro.git $ cd muro $ mix test $ mix muro.check examples/half_ok.muro