Li Language Design Spec¶

Date: 2026-05-14 (rev. 5)
Status: Planning
Milestone: Tetris + proved physics kernels — unproved code does not compile License: Apache-2.0 OR MIT (open source)

Vision¶

Li is an open-source, compiled, Nim-syntax language for HPC and scientific computing. Its reason to exist is mathematical provability: every shipped program is a theorem the Lean 4 kernel accepts — not a program we merely tested or type-checked.

Easy syntax and fast execution are co-equal product goals, but neither may weaken the proof gate. If a feature cannot be made provable, it does not ship in user code.

The three pillars (priority order)¶

flowchart TB
    P1["1. Mathematical provability<br/>Lean 4 · contracts · totality · refinements"]
    P2["2. Easy syntax<br/>Nim-like · Python 3.14 types"]
    P3["3. Fast execution<br/>LLVM · SIMD · parallel for"]

    P1 --> P2
    P1 --> P3

Conflict resolution (binding)¶

When pillars collide, follow this order:

1. Provability wins — drop or redesign the feature (e.g. no Any, no unproved parallel for, no unsafe).
2. Syntax yields — add sugar only if elaboration to Core is proved sound in Lean.
3. Speed yields — -O3, SIMD, and OpenMP apply after verification; never skip Lean for release builds.

The only unproved surface is docs/semantics/trusted.lean (minimal IO + audited extern). That file is capped and RFC-reviewed; it is not a loophole for user logic.

What “mathematically provable” requires (checklist)¶

Every compiling module must have:

• Python 3.14 typing (no Any) + refinements where values carry predicates
• requires / ensures on every proc
• invariant + decreases on every loop (while, parallel for)
• Memory safety via borrow rules (no UB in accepted programs)
• All proof obligations discharged in Lean 4 (Coq-grade kernel, not SMT-only)
• Parallel loops: proved iteration independence on shared memory
• No sorry, assume, or bare cast in user source

lic check is IDE convenience only. lic build is the proof certificate.

Non-negotiables¶

Compiler stack¶

Rejected hosts: Zig (explicit), Rust for v0 (slow linker iteration on a large LLVM-linked binary — revisit only if team prefers it).

Rejected backends: Cranelift — one IR, one optimizer, one mental model.

Bootstrap path: C++ → Li (same pattern as Clang → eventually self-host, or OCaml → Rust historically).

Python 3.14 type catalog (li mapping)¶

Reference: Python 3.14 typing, annotationlib, whatsnew 3.14.

3.14-specific behavior to implement¶

Scalar & builtin types¶

Collections (PEP 585 builtins)¶

Special typing forms¶

Generics (PEP 695)¶

type Vec[T] = object
  data: ptr T
  len: int

proc map[T, U](xs: list[T], f: proc(x: T) -> U) -> list[U] = ...

• TypeVar, TypeVarTuple, ParamSpec, Concatenate, Unpack — all supported in checker
• Deprecated Generic[T] class syntax → PEP 695 type / bracket params only

Protocols & ABCs (PEP 544, collections.abc)¶

Structural typing for: Iterable, Iterator, Sized, Callable, Mapping, Sequence, Hashable, Awaitable, AsyncIterator, ContextManager, Reader, Writer, and Protocol user types.

Nominal: object inheritance still primary for li object/enum.

Callable¶

Callable[[A, B], R] and proc(a: A, b: B) -> R interchangeable in annotations.

ParamSpec for decorators: Concatenate[Lock, P] patterns.

TypedDict, NamedTuple¶

type Point = tuple[x: float, y: float]  # NamedTuple

type Config = typedict
  host: str
  port: NotRequired[int]

Enums¶

enum, IntEnum, StrEnum, Flag — Nim enum + backing type annotations.

Generators & async¶

Scientific / HPC extensions (beyond Python)¶

See Numeric roadmap for full scalar schedule. Summary:

Deprecations we skip (not in li)¶

• typing.IO / TextIO / BinaryIO → use Reader/Writer
• typing.Generic old syntax → PEP 695 only
• typing.AnyStr → class C[T: (str, bytes)]
• typing.TypeAlias assignment form → type statement
• Runtime isinstance on complex typing objects — li is static; runtime reflection limited

Numeric roadmap¶

Li numerics are Python 3.14 at the surface (names and habits) but compiled and fixed-width under the hood. This section is the single source of truth for scalar types, overflow, operators, and what ships when.

Phase 1 — v1 scalars (Tetris + typechecker)¶

Default types (Python names → machine types)¶

Fixed-width types (explicit HPC/systems)¶

No silent widening: i32 + i64 is a type error unless explicitly cast.

Overflow modes¶

Applied per type (e.g. wrapping i32, checked int):

Literal suffixes¶

42       # int   → i64
42u      # uint  → u64
42i32    # i32
42u8     # u8
3.14     # float64
3.14f32  # f32
2.0 + 1.0i   # complex128

Operator rules (v1)¶

Effects tied to numerics¶

SIMD vectors (v1)¶

Explicit packed lanes for HPC kernels. Scalar loops may still auto-vectorize via LLVM; simd types are for deterministic lane-wise code.

type Vec4f = simd[f32, 4]
type Vec8f = simd[f32, 8]
type Vec4i = simd[i32, 4]

proc add(a, b: Vec4f) -> Vec4f =
  return a + b   # elementwise; lowers to LLVM vector add

proc dot(a, b: Vec4f) -> f32 =
  return horizontal_sum(a * b)

Stdlib (v1): horizontal_sum, horizontal_max, fma, shuffle, blend, dot for simd[f32/f64, N].

Codegen: MIR simd ops → LLVM vector types (<4 x float> etc.); ISAs: x86 SSE/AVX/AVX-512, AArch64 NEON. Milestone: SIMD micro-benchmark beats equivalent scalar loop at -O2.

Explicitly not in v1¶

• unchecked int, runtime-only bounds without proof
• SIMD without target proof or explicit requires alignment preconditions

Phase 2 — half precision¶

f16 / bf16 (16-bit floats)¶

Requires: hardware feature detection, explicit conversion rules (f32 ↔ bf16 never silent in narrowing direction), and LLVM FP16/bf16 codegen support on target triple.

Phase 3 — shaped arrays & GPU¶

Depends on Phase 1 numerics (including SIMD) and a stable MIR → LLVM path (or secondary GPU IR).

Phase 4 — exact & extended numerics (scientific stdlib)¶

These live in std, not the language core. The compiler only needs stable scalar and tensor foundations.

Roadmap summary¶

flowchart LR
    P1[Phase 1<br/>scalars complex simd]
    P2[Phase 2<br/>f16 bf16]
    P3[Phase 3<br/>tensor GPU]
    P4[Phase 4<br/>BigInt Rational units linalg]

    P1 --> P2 --> P3 --> P4

Data structures roadmap¶

Python’s dict is a hash table — we expose one user-facing dict[K,V] type (open addressing or Swiss-table style internally; not a separate public Hashtable type). Same for set[T]. This section lists every aggregate the language and stdlib need, when they ship, and how memory works.

Terminology¶

Phase 1 — v1 (Tetris + core checker)¶

Built into the language or minimal std — enough to write games and typed algorithms.

Fixed arrays — array[N, T]¶

type Board = array[20, array[10, Cell]]
var row = board[3]
board[3][4] = Cell(color: Cyan)

• N must be a compile-time constant
• Literal index out of range → compile error
• Dynamic index requires refinement type or proof — no unproved runtime-only bounds in release builds
• Multidimensional = nested array, or row-major flat array[N*M, T] in std

SIMD + parallelism (v1)¶

Packed lanes and parallel for are both v1. See Parallelism & multi-core execution (v1).

Product & sum types¶

Strings & byte buffers¶

Heap collections (Python names, explicit allocation)¶

All heap collections require effect raises Alloc on growth. Iteration borrows immutably; mut access needs borrow mut or owned value.

Typed records¶

type Config = typedict
  host: str
  port: NotRequired[int]
  token: ReadOnly[str]

Structural dict type for APIs — compile-time field checking, lowered to dict[str, T] or struct at runtime (implementation choice; checker enforces fields either way).

Hashing contract¶

type Hash = trait
  proc hash(self: Self) -> u64
  proc eq(self: Self, other: Self) -> bool

dict/set keys must implement Hash (nominal object/enum derive automatically; newtypes opt in).

What v1 does not include¶

• deque, OrderedDict, Counter, defaultdict (stdlib Phase 2)
• tensor / n-dimensional heap arrays
• Linked lists, trees, graphs (stdlib only, if ever)
• Weak references, GC’d shared mutability

Phase 2 — Python stdlib parity & algorithmic containers¶

Also: sort, binary_search, heap_push/pop on slices and lists.

Phase 3 — HPC & scientific shapes¶

GPU side (with numeric Phase 3):

Phase 4 — advanced & domain structures¶

Only added when a real benchmark or library needs them — not language builtins.

Memory & safety rules (all phases)¶

Roadmap summary¶

flowchart LR
    D1[Phase 1<br/>array simd parallel list dict]
    D2[Phase 2<br/>deque OrderedDict heap]
    D3[Phase 3<br/>tensor sparse arena GPU buffers]
    D4[Phase 4<br/>BTree Arc Graph Channel]

    D1 --> D2 --> D3 --> D4

Parallelism & multi-core execution (v1)¶

Li v1 ships CPU multi-core parallelism, not only SIMD. HPC without parallel for is a non-starter. Parallelism stays provable-only: races and unsynchronized shared mutation are compile errors.

Three layers¶

parallel for (v1)¶

parallel for i in 0..<N
  requires disjoint_tile(i, grid)
  ensures tile_ok(i, grid)
  decreases N - i
=
  compute_tile(grid, i)

lic build --threads=N sets OpenMP team size (default: machine cores).

Provable-only rules (v1)¶

• parallel for rejected unless Lean discharges iteration independence (disjoint indices / immutable shared read).
• borrow mut across iterations rejected without disjointness proof.
• Read-only parallel loops over borrow imm / immutable data: always allowed.

Borrow + parallel (v1 MD pattern)¶

# Positions immutable this step; forces written to disjoint f[i]
parallel for i in 0..<N
  requires forall j, k, tile(i, j) and tile(i, k) and j != k ==> force_index(j) != force_index(k)
  decreases N - i
=
  compute_force_i(positions, forces, i)

SIMD + multi-core together (v1)¶

Inner loop: simd; outer loop: parallel for. Standard li HPC idiom — both required in v1 benchmarks.

GPU (not v1)¶

gpu proc and devicebuffer remain Phase 4+. v1 competes on multi-core CPU + SIMD vs C++/Rust/Julia.

Benchmarks (v1)¶

Tier 2 (three_body, md_lennard_jones) must ship proved parallel for li builds before perf tables. Report 1-thread and N-thread columns from day one of v1.

Shared memory model (v1)¶

OpenMP worker threads share one process address space (POSIX shared memory). Li does not expose raw threads or locks in v1; shared RAM is accessed only through constructs the compiler can prove race-free.

Guarantee (v1): If lic build succeeds, the program has no data races on user var / mutable buffers under the Li memory model. Violations are compile errors, not TSan surprises at runtime.

Debug-only: LI_RT_TSAN=1 links ThreadSanitizer on CI nightly to catch compiler bugs — not a user safety net.

Race-reject test suite (v1, mandatory CI)¶

Deliberate exploit attempts in li-tests/race_shared_memory/*.li must fail lic build with a diagnostic citing shared memory / disjointness / Send / Sync. Run on every PR:

./li-tests/run_all.sh race_shared_memory
# or: ./scripts/test_race_reject.sh

Positive control: li-tests/race_shared_memory/good_disjoint_parallel.li must lic build — paired MD tile loop with valid proof.

Contracts & formal verification (provable-only)¶

If Lean does not accept the proof, lic build fails. There is no optional verification tier, no unsafe, no sorry, no Any, no bare cast.

Li combines Python 3.14 types (minus Any), mandatory Hoare contracts, refinement types, totality, and Lean 4 kernel checking — the same assurance class as Coq / Lean total correctness (not SMT-only).

Coq: Lean 4 is the primary proof engine. Coq export remains Phase 7+.

What may compile¶

What is forbidden in source¶

Trusted base (only escape hatch)¶

The only unproved code is the minimal trusted runtime axiomatized in docs/semantics/trusted.lean:

• IO primitives (read_input, present_frame, SDL hooks) as abstract monad axioms
• Alloc allocator laws (or no heap until alloc proofs exist)
• LLVM codegen correctness (until translation validation proves preservation)

All user .li modules — including Tetris logic and physics kernels — must prove. The game step function is proved; the OS loop calls it via trusted IO.

Contract syntax (mandatory on every proc)¶

proc sqrt(x: float) -> float
  requires x >= 0.0
  ensures result >= 0.0
  ensures abs(result * result - x) < 1e-12
  decreases 0
=

proc verlet_step(
    pos: var tensor[(N, 3), f64],
    vel: var tensor[(N, 3), f64],
    dt: f64
) -> unit
  requires dt > 0.0
  requires N > 0
  ensures abs(total_energy(pos, vel) - old(total_energy(pos, vel))) <= energy_bound(dt)
  decreases 1
=
  var i: {k: int | 0 <= k and k <= N} = 0
  while i < N
    invariant 0 <= i and i <= N
    invariant symmetry_momentum(pos, vel)
    decreases N - i
    ...
    i += 1

Refinement types (proof-carrying)¶

type PosInt = {x: int | x > 0}
type Index20 = {i: int | 0 <= i and i < 20}

proc row(board: Board, i: Index20) -> array[10, Cell]
  ensures true
  decreases 0
=
  ...

Dynamic indices become refinements or explicit proof terms — no silent runtime-only checks in compiled release code without a proved bound.

Proof blocks¶

theorem energy_bounded(dt: f64) -> unit
  requires dt > 0.0
  ensures ...
  decreases 0
  = proof
    ...
  qed

All theorem / lemma bodies must compile to closed Lean terms. No sorry.

Compilation pipeline (proof is not optional)¶

.li
  → parse → typecheck (no Any)
  → contract + totality well-formedness
  → VC generation → Lean 4 goals
  → lean (kernel) — **STOP if any goal open**
  → borrow check → MIR → LLVM

What Lean proves¶

Honesty boundary¶

• Provable = your specs + Lean agree; wrong ensures → wrong theorem.
• Trusted = only trusted.lean + audited extern contracts — keep this surface tiny.
• The C++ compiler implementing the pipeline is not meta-proved yet.

Compiler pipeline¶

.li
  → lex → parse → name resolve
  → deferred annotation resolve (PEP 649 style)
  → typecheck (Python 3.14 − Any + refinements)
  → mandatory contracts + totality check
  → VC generation → Lean 4 kernel (**hard gate**)
  → borrow check → MIR (simd + **parallel** regions) → LLVM IR + OpenMP
  → link li_rt (trusted IO only)

Repository layout (C++)¶

li/
  compiler/           # C++17: lexer, parser, types, mir, llvm_codegen
  runtime/li_rt.c
  std/                # li standard library (.li)
  lib/                # shipped as bitcode or source
  examples/tetris/
  benchmarks/           # perf harness (see also li-tests/benchmarks/)
  li-tests/          # **all conformance tests** — manifest.toml + run_all.sh
  docs/semantics/     # Lean 4
  LICENSE-MIT
  LICENSE-APACHE

Phased delivery (realistic)¶

Benchmark plan: docs/superpowers/plans/2026-05-14-benchmarks-and-simulations.md

Validation suite (beyond Tetris)¶

Cross-language comparisons use shared params.toml, correctness invariants before timing, single- and multi-thread columns.

Tetris success criteria¶

• lic build examples/tetris/main.li -o tetris --release
• Board array[20, array[10, Cell]] literal OOB → compile error
• lic check < 500ms on tetris sources
• Parity tests: subset of typeshed stubs typecheck equivalently (mypy baseline)