len¶

A specification-first language for programs about programs¶

len is a meta-programming language for writing systems that generate, transform, or reason about code structures.

Instead of treating the specification as a comment written after the fact, len makes it the primary artifact. You state the model, the relations, and the laws first, then connect executable forms to those declarations.

Read the concepts guide Start with Hello World

:material-compass-outline: Orient yourself

Understand the language model, module system, and layer boundaries.

Open Concepts
:material-play-circle-outline: Build and validate

Install the toolchain and run your first .l1 file through the validator.

Open the Hello World tutorial
:material-book-search-outline: Look up syntax

Jump straight into reserved words, grammar, and language surface details.

Open the reference
:material-console-line: Use the CLI

See command syntax, exit codes, diagnostics, and validation behavior.

Open the CLI reference

Where to Start¶

Goal	Start here
Understand what len is and why it exists	Concepts
Install and run your first program	Hello World tutorial
Look up a specific keyword	Keywords reference
Use the command-line tool	CLI reference
Come from a Java background	Coming from Java
Generate a PostgreSQL schema	Postgres shop tutorial

Language Layers¶

len is organised into three levels:

Level	Name	Purpose
l0	Natural	Informal pseudocode, design notes, brainstorming
l1	Structural core	Types, relations, formulas, specifications
l2	Evaluation	Contexts, satisfaction, executable semantic rules

Most day-to-day work happens in l1. Files carry the extension .l1.

Quick Taste¶

import core.math.set

type Point

rel OnCircle(p: Point, radius: Nat)

spec circle_definition
    given p: Point
    given r: Nat
    must OnCircle(p, r) iff
        exists x: Nat, y: Nat .
            At(p, x, y) and x * x + y * y = r * r

Documentation Map¶

Tutorials¶

Hello World — install, build, validate
Types and Relations — core modelling primitives
Writing Specifications — axioms, definitions, and laws
Functions and Quasi — executable forms and pseudocode
Contracts and Structs — grouping and record types
Coming from Java — map OOP ideas into len
PostgreSQL Schema Generation — generate an online shop schema

Reference¶

Concepts — philosophy, layers, and the module system
Keywords — reserved words and their meanings
Syntax — grammar, operators, and sugar forms
CLI — len-cli command reference