Li — a compiled, high-performance, proofable language for science, engineering, and AI

The priority

Correct first. Readable next. Fast last.

Li will not trade a wrong answer for a quicker one. The program has to check out, it has to be easy to read, and only then does it compile to native speed.

1 · first

It has to be true

A function can say what it needs and what it promises. A loop can say why it finishes. If two parallel pieces would overwrite the same memory, the build stops.

The build command is lic build.

2

It has to read easily

The code looks like Python or Nim: indentation, def, types like list[T]. Names stay close to the science.

Shortcuts only if they still check out.

3

Then it can be fast

You write the math. The compiler handles the rest.

A speed flag never skips the check.

Examples

Write the limits next to the code.

Open the orbit tab. The time step has to be greater than zero. After the update, energy cannot have drifted too far. You put those facts in the function, not in a comment. The compiler checks them when you build. requires is the before. ensures is the after.

              
              
              
              
            

              hello.li
              
            

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

              def advance_orbit(body: Body, dt: float) -> unit
  requires dt > 0
  ensures energy_drift(body) < max_drift
  decreases 0
=
  var force: Vec3 = gravity_from(body.position)
  body.velocity = body.velocity + force * dt
  body.position = body.position + body.velocity * dt
            

              def dot4(x: array[4, float], y: array[4, float]) -> float
  requires true
  ensures result == x[0] * y[0] + x[1] * y[1] + x[2] * y[2] + x[3] * y[3]
  decreases 0
=
  return x @ y
            

              def main() -> int
  requires true
  ensures result == 0
  decreases 0
=
  var buf: array[8, float]
  parallel for j in 0..<8
    requires disjoint_elem(j, buf)
    decreases 8 - j
  =
    buf[j] = 0.0
  return 0
            

How it compiles

Check while you write. Build to run.

Two commands. One is a quick look while you type. The other is the real compile. Only the real compile makes a program you can run, and only after the checks pass.

Makes a program

lic build

This is the compile you ship. It checks the file, then writes a binary.

Editor only

lic check

Fast feedback while you type. Useful in the editor. It does not replace build.

These are not in the language:

Any unsafe sorry assume bare cast unproved parallel for

Who it’s for

People who run the numbers. Models that write the files.

If you simulate heat, orbits, robots, or games, Li is meant to be the language you ship, not a notebook you later rewrite in C. If a chat writes the first draft, the same file still has to check. That is how AI coding becomes software you can keep, not a pile of guesses.

Simulation

The same file as the run

Orbits, molecules, heat, waves. The first sketch and the fast version can be the same .li file.

Science

The physics stay in the code

You can write that an index stays in range, or that energy does not drift too far. That sits next to the update, not in a paper beside it.

Agents

The model is not the proof

An LLM can write the update. It cannot skip the rules. lic build checks the file. Trust that, not the prompt.

AI coding

Let the model write. Ship only what checks.

A lot of AI coding looks finished and is not. The chat invents a time step, a loop that never ends, or two threads that write the same memory. In an ordinary language you find that later. In Li those limits sit in the file, and lic build has to accept the file before you get a program.

That is the point of an AI-first language for science and engineering: the model writes the same syntax a person would, and the compiler is what makes the software solid. You do not trust the prompt. You trust the check.

Write

Same language for both

Indentation, def, names from the science. A model writes the same .li a person would. There is no second dialect for chats, and no hidden Any.

Check

The build is the gate

Before a function runs, some facts must already be true. After it returns, some facts must still be true. A loop must finish. The compiler accepts or rejects. There is no sorry to cover a guess.

Ship

Solid means it built

If the file builds, you have a native program with the limits still in it. If it does not, the model has to fix the file, not explain the bug in prose.

Hand a chat llms.txt and the agent handbook. Those are markdown on purpose. Do not scrape the styled docs.

Get started

Install it. Run hello.

Most people start with the installer. To build from source you need LLVM, CMake, and a C++ compiler. Versions are in the getting-started guide.

Linux · macOS · WSL

$ curl -fsSL https://lilangverse.xyz/cli/install.sh | bash

Windows

irm https://lilangverse.xyz/cli/install.ps1 | iex

from source

$ git clone https://gitlab.lilangverse.xyz/li-langverse/lic.git
$ cd lic
$ ./scripts/build.sh
$ ./build/compiler/lic/lic build hello.li -o hello
$ ./hello

Where it is

Useful now. Honest about the rest.

lic already checks types and memory, and can emit native code for a growing set of programs. The full mathematical proof step is still being built. Today build rejects problems it can see. The rest is listed in the provability gaps.

Open source. MIT or Apache-2.0. The handbook is markdown so a chat can ingest it. Start at llms.txt.

See the compiler

Write the rulesinto the program.