(Work in progress)
Tibi is a toy programming language with its interpreter and compiler implemented in Lean 4.
Features:
- Statically typed: ensures type safety at compile-time.
- Formally verified:
- Interpreter: correctness and completeness of evaluation on type-checked source code.
- Compiler: semantic consistency with the target WebAssembly (Wasm) binary.
Tibi's interpreter and compiler can be used by either lake exec tibi or ./lake/build/bin/tibi (after running lake build).
This requires Lake, the package manager for Lean 4.
Tibi can execute a Read-Eval-Print Loop (REPL).
$ lake exec tibi
0:> 42
- : Int = 42
1:>Tibi can compile to Wasm. Here's how you compile a simple Tibi script:
$ cat test.tibi
1
$ lake exec tibi test.tibi >test.wasm
$ hexdump -C test.wasm
00000000 00 61 73 6d 01 00 00 00 01 05 01 60 00 01 7e 03 |.asm.......`..~.|
00000010 02 01 00 07 08 01 04 6d 61 69 6e 00 00 0a 06 01 |.......main.....|
00000020 04 00 42 01 0b |..B..|
00000025
$A compiled Wasm binary exports a single function named main, that takes no arguments and returns a single integer.
To execute this, you can use the following HTML:
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<title>Wasm Test</title>
</head>
<body>
<pre id="output"></pre>
<script>
WebAssembly.instantiateStreaming(fetch("test.wasm")).then(
(obj) => { document.getElementById('output').innerText = obj.instance.exports.main() },
);
</script>
</body>
</html>You can see the returned integer in the pre element.
ws = { " " | "\n" | "\r" | "\t" } ;
non-zero-digit = "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" ;
digit = "0" | non-zero-digit ;
nat-number = "0"
| non-zero-digit , { digit } ;
sign = "+" | "-" ;
int-number = sign , nat-number ;
expr = nat-number , ws
| int-number , ws;If Tibi's expressions are typable, their evaluation succeeds and evaluates in a value of the corresponding type.
Tibi.type_safe provides proof of the following statement:
where
-
$\vdash e : \tau$ denotesTibi.HasType e τ, and -
$\vdash e \Downarrow r$ denotesTibi.Eval e r,
When expressions in Tibi that are typable are compiled into Wasm binaries,
the semantics of Tibi must align with the semantics of Wasm to ensure consistency.
Wasm.Reduction.of_has_type_of_eval_ok_of_compile_ok provides proof of the following statement:
where