Li¶
理 — principle, reason. Source files: .li. Compiler: lic.
-
:material-shield-check:{ .lg .middle } Prove it
Lean 4 kernel, mandatory contracts. No binary without proof.
-
:material-feather:{ .lg .middle } Write it easily
Nim-like syntax, Python 3.14 types — without
Any. -
:material-lightning-bolt:{ .lg .middle } Run it fast
LLVM 18, SIMD, OpenMP — only after the proof gate passes.
The proof gate¶
lic build module.li # types + memory + contracts + Lean → binary or REJECT
lic check module.li # IDE only — not a certificate
Every proc carries requires / ensures; every loop carries invariant / decreases. Forbidden: Any, unsafe, sorry, bare cast, unproved parallel for.
Three pillars (strict priority)¶
| # | Pillar | Rule |
|---|---|---|
| 1 | Mathematical provability | Never compromised |
| 2 | Easy syntax | Nim-like, Python 3.14 − Any |
| 3 | Fast execution | LLVM — only after proof |
Quick start¶
export LLVM_DIR="$(brew --prefix llvm@18)/lib/cmake/llvm" # macOS
export CC=clang CXX=clang++
./scripts/build.sh
./build/compiler/lic/lic --version
./scripts/local-ci.sh
See Getting started for Linux prerequisites and repo layout.
Where to go next¶
| Topic | Page |
|---|---|
| Compile pipeline | Architecture |
| Lean gate & contracts | Verification |
| Type system & numerics | Language design spec |
| Implementation order | Master plan |
| Physics & perf harness | Benchmarks |
| All tests | li-tests on GitHub |
Status¶
Phase 0–3 bootstrap: C++ lic parses, typechecks, and emits LLVM for a growing subset. Self-host and full Lean pipeline are on the roadmap.