Home

理

Li · prove · write · run fast

Li is a language for programs you can trust in production: contracts checked before ship, memory and parallelism ruled out as failure modes, and native speed when the proof closes.

:material-hand-wave:{ .lg .middle } New here?

Start with Hello world, Math-first HPC examples, and the Examples gallery.
:material-book-open-variant:{ .lg .middle } Learn the language

Language handbook — types, numbers, SIMD, parallel, contracts.
:material-cog:{ .lg .middle } How the compiler works

Build pipeline and Why provable.
:material-shield-check:{ .lg .middle } Trust but verify

All tests and Security audits.

Three promises¶


Prove it	Target: `lic build` fails if proofs do not close. Today: static gate; gaps.
Write it easily	Readable syntax; Python-like types without `Any`.
Run it fast	LLVM + SIMD + `parallel for` after proof.

Quick example¶

def main() -> int
  requires true
  ensures result == 0
  decreases 0
=
  echo "Hello from Li"
  return 0

Install and build¶

Getting started — tools

Full documentation map¶

Section	Contents
Guide	Tutorials and copy-paste examples
Language	Every type, feature, and rule
Compiler	Compile-time behavior
Testing	Suites, fuzz, CI, audits
Provability gaps	What is not proved/wired yet (honest status)
Ecosystem	Packages, `lip`, governance (`li-langverse`)
Creating packages	`li-new-package` scaffold
Reference spec	Normative design (technical)

Project status¶

The compiler is under active development. Phase tracker: Master plan. What proofs exist today: Provability gaps. Native HPC (SIMD + OpenMP): Phase 7 plan.