Home

理

理 · reason

Li is a compiled language for science and simulation. You write ordinary code, then you write what has to stay true. If that doesn’t hold, Li will not give you a program.

New here?

Start with Hello world, Math-first HPC examples, and the Examples gallery.
Learn the language

Language handbook — types, numbers, SIMD, parallel, contracts.
How the compiler works

Build pipeline and Why provable.
Trust but verify

All tests and Security audits.
Agents and chats

Fetch llms.txt, not the HTML. How to ingest this handbook.

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
For agents	`llms.txt`, raw Markdown, handover
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.