LOGOS Syntax Guide

What is LOGOS?

LOGOS is a programming language where you write code in natural English. Instead of cryptic symbols and arcane syntax, you express your ideas in sentences that read like plain prose—and those sentences compile into efficient, executable programs.

LOGOS has two modes:

This guide focuses primarily on Imperative Mode—using LOGOS as a programming language. Part VI covers Logic Mode and verification for those interested in formal semantics.

The Vision

The name LOGOS comes from the Greek λόγος, meaning "word," "reason," and "principle." In LOGOS, these concepts unify:

• Words become executable code
• Reason becomes verifiable logic
• Principles become formal proofs

When you write LOGOS, you're not writing comments that describe code—you're writing sentences that *are* the code.

How to Read This Guide

If you're new to programming:

• Read each section in order
• Try every example yourself
• Don't skip ahead—each concept builds on the previous

If you're an experienced programmer:

• Use the Table of Contents to jump to what interests you
• The Quick Reference section provides rapid lookup
• The Complete Examples show real-world patterns

The phrasing you would guess

LOGOS is a deterministic grammar, not an AI guessing your intent. Every sentence the

parser accepts has exactly one meaning, and the design rule is least surprise: the

phrasing you would naturally write is the phrasing that works. Where several natural

phrasings exist, they are synonyms for the same operation — 2 + 3 and 2 plus 3

compile to the same addition, and neither is more "real" than the other.

English first, symbols beside

Every operator has an English form and a symbolic twin: plus and +, is at least

and >=, equals and ==. Use whichever reads better in context; they are the same

program. The full table lives in Operators and Expressions.

The deliberate exceptions

A few places where LOGOS chooses the human reading over programmer tradition — learn

these and the rest of the language follows your intuition:

• Counting starts at 1. item 1 of items is the first element, and slices are

inclusive on both ends: items 1 through 2 is two elements.

• Equality has a canonical spelling: equals (or ==). Bare is also

compares — x is 5 runs and is true — but is wears many hats in LOGOS

(descriptions, definitions, predicates like is even), so this guide writes

equals wherever equality is meant: the dedicated spelling keeps intent

unambiguous.

• Fields read as possessives. A struct's field is alice's age — the apostrophe

is grammar, not decoration.

The examples below preview indexing, comparisons, and If — each is taught fully in

Part II; here they carry the mental model only.

*Try it: in the first example below, change plus to times — then make the symbolic

line disagree and watch the last line turn false.*

Installing largo

Everything on this site runs in your browser — but for real projects you want largo,

the LOGOS build tool, on your machine. One line, no toolchain required:

curl -fsSL https://logicaffeine.com/install.sh | sh

On Windows:

powershell -ExecutionPolicy Bypass -c "irm https://logicaffeine.com/install.ps1 | iex"

The installer fetches the prebuilt binary for your platform (Linux/macOS x64 + arm64,

Windows x64), verifies its SHA-256 checksum, and installs it to ~/.local/bin — no sudo,

no shell-config edits. Add --full (sh -s -- --full) for the build with Z3 verification

bundled. Then:

largo new hello && cd hello && largo run

Hello World

Every programming journey begins with Hello World. In LOGOS:

The Program Structure example below is a deliberate preview — a struct and a function

before either is taught. Every piece gets its full section in Part II; here it shows

the shape of a real program.

One small program, built in five stages — each stage runs, and each adds exactly one idea.

The game: you think of a number between 1 and 100; the *program* finds it by binary

search, and it never needs more than 7 tries.

Stage 1 sets the scene with variables and Show. Stage 2 makes one guess: the

midpoint, and an If to say which way it missed. Stage 3 turns that into the whole

game with While and Break, halving the range each round. Stage 4 extracts a

function so any secret can be found. Stage 5 packages the result in a struct and

announces it with interpolation.

The secret is written into the program so every stage runs right here — change it at any

stage and watch the search adapt. Every construct the game uses — While, Break,

functions, structs, interpolation — gets its full treatment in Part II; the tutorial

shows them working together first.

*Try it: in Stage 4, try secrets 1 and 100 — the edges. Does it ever need more than 7?*

Look back: the halving move generalizes to any sorted search — dictionaries,
version bisecting, guess-the-bug. What breaks if the range starts at 0? Nothing —
but if the secret is OUTSIDE the range, the loop never ends: bounds are the
contract. Try counting comparisons instead of tries.

Part I is done — prove it to yourself. The three challenges below blend what you

met across the part: the program shape, the twin spellings, and the tutorial's

midpoint arithmetic. Then the recall cards collect on the part's promises.

Nothing here is new. If a challenge stumps you, the section to reread is named

in its hints — that is the point of a checkpoint.

Variables are containers that hold values. In LOGOS, you create and modify variables using natural English sentences.

Creating Variables

Use Let to create a new variable. The word be assigns a value to the variable.

Changing Values

Use Set to change an existing variable. The difference between Let and Set:

• Let creates a *new* variable
• Set modifies an *existing* variable

Let mutable x be 0. flags a binding you intend to reassign — loop counters, running

totals. The checker does not currently reject Set on a plain Let, so the mutable

is for your reader: it marks the moving parts.

Primitive Types

Decimal literals have type Real, and Float is another name for exactly the same type —

either annotation accepts them.

Characters (Char)

Characters represent single Unicode characters, wrapped in backticks. See the example below.

Bytes (Byte)

Bytes are 8-bit unsigned integers (0-255), useful for binary data and low-level operations.

Type Annotations

Usually, LOGOS infers the type from the value you assign. But you can be explicit with : Type.

The exact numeric tower

---

Nat — counts by intent

Annotate : Nat for values that are counts: Let count: Nat be 5. documents that the

number is never meaningfully negative.

Rational — exact fractions

A Rational does arithmetic exactly — no rounding, ever. Give a value the annotation and

every division stays a true fraction: half of 7 plus a third of 7 is exactly 35/6, not

5.8333….

BigInt — integers that never overflow

When Int arithmetic exceeds 64 bits, LOGOS promotes the result automatically instead of

wrapping or crashing. The example below adds 1 to the largest 64-bit integer — the sum no

64-bit integer can hold — and prints it exactly.

Decimal — money-grade exactness

Binary floats cannot represent one tenth: 0.1 + 0.2 famously prints

0.30000000000000004. decimal("0.1") is exact base-10 arithmetic — the same sum is

exactly 0.3. When the number is money, use decimal (or the Money type).

Complex

complex(re, im) builds an exact complex number: complex(0, 1) is the imaginary unit,

and squaring it gives -1.

The math toolbox

sqrt(x), floor(x), ceil(x), round(x), pow(a, b), abs(x), min(a, b),

max(a, b) — all built in, no import needed.

*Try it: in the Decimal example, add a third decimal("0.1") to the sum — then try the

same with plain floats and compare.*

Time, money, and measures

---

Time

• 500ms, 2s, 5min — a Duration (SI time).
• 2026-05-20 — a Date.
• 4pm, 9:30am, noon — a Time of day.
• 2 weeks, 3 months — a calendar Span.

Calendar extractors read components: year_of(d), month_of(d), day_of(d),

weekday_of(d).

Money

$19.99, €5, £10 — exact amounts in a real currency, quantized to the currency's

minor unit. No float cents, ever: $19.99 + $0.01 is exactly 20.00 USD, and splitting

a bill rounds to real cents.

Quantities

quantity(3, "meter") is a dimensioned physical value. Adding a length to a time is not

a rounding error — it is a caught, impossible operation (run the mismatch example).

Identifiers

uuid("…") parses an RFC 9562 UUID; uuid_version(id) reads its version nibble.

Pausing

Sleep 2ms. (or Sleep 500. — milliseconds) pauses the program.

*Try it: change the bill split to four ways — where does the remainder cent go?*

The complete type map

Every type in the language, in one place. The ones marked with a section name get their

deep dive there; everything else is taught right here.

Strings in LOGOS are Text. Build them by concatenation or — usually better — by

interpolation: write the variable inside braces and it renders in place.

Interpolation

"Hello, {name}!" inserts name's value. A format spec after a colon controls the

rendering: "{pi:.2}" rounds to two decimal places. And "{v=}" is the print-debugging

form — it renders as v=42, the name and the value together.

Braces evaluate names and arithmetic: "{a + b}" renders the sum. English operator

phrases are the exception — "{length of tasks}" does not parse inside braces. Compute

those first (Let n be length of tasks.), then interpolate the name: "({n})".

Joining sequences

+ concatenates Text. Sequences join with followed by: a followed by b is one new

sequence with b's elements after a's.

Characters

A Char is a single Unicode character in backticks: a , \n , \t .

*Try it: in the format-spec example, change .2 to .4 — then remove the spec entirely.*

Operators let you combine values into expressions. LOGOS supports both symbolic operators (like +) and English words (like plus).

Arithmetic

Comparisons

Logical Operators

Control flow determines which code runs and in what order. LOGOS provides conditionals and loops using natural English syntax.

Conditionals

Use If to execute code only when a condition is true. The colon (:) after the condition opens an indented block.

If/Otherwise

Use Otherwise to handle the false case.

While Loops

Use While to repeat code as long as a condition is true.

For-Each Loops

Use Repeat for to iterate over collections.

Functions are reusable blocks of code. In LOGOS, you define functions using natural English headers that describe what the function does.

Defining Functions

A function definition starts with ## To followed by the function name.

Parameters

Functions can accept parameters—values passed in when the function is called. Separate

them with and in the definition (commas also parse; the guide writes the English form).

Calls use commas: add(3, 5).

Return Values

Use -> Type to specify what the function returns.

Recursion

Functions can call themselves. This is called recursion. Every recursive function needs:

• A base case — when to stop recursing
• A recursive case — calling itself with a "smaller" problem

Functions are values. A closure is a function written inline — bind it to a name, pass it

to another function, return it.

Expression closures

(x: Int) -> x + 1 is a complete function: one parameter, one expression, the result is

the return value.

Block closures

When the body needs statements, write ->: and indent — the block form.

Functions that take functions

A parameter typed fn(Int) -> Int accepts any matching closure. This is how map/filter

pipelines and callbacks are built.

Mental model: A closure is a recipe card that also photographs the pantry:
(x: Int) -> x + n copies the value n holds at the moment the card is written.
Reassign n later and the card still cooks from the photograph, not the shelf.
The photograph is not the whole kitchen, though — parameters still arrive fresh
on every call.

*Try it: in the last example, swap the doubling closure for (n: Int) -> n * n.*

Collections hold multiple values. LOGOS provides four main collection types:

Creating Lists

Create a list with square brackets, or create an empty list with a type.

Accessing Elements

LOGOS uses 1-based indexing. The first element is at position 1, not 0. Why? Because that's how humans count.

Modifying Collections

• Push to add an element to the end
• Pop to remove and get the last element
• copy of to create a deep copy

Slicing

Extract a portion of a list with through. Slicing is inclusive on both ends.

Maps (Dictionaries)

Maps store key-value pairs. Unlike lists which use integer indexing, maps use keys of any type.

Create a map:

Let prices be a new Map of Text to Int.

Access a value by key:

Let cost be prices["iron"].

Set a value by key:

Set prices["iron"] to 100.

Maps are useful for lookups, caches, and associating data without needing a struct.

Bracket Syntax

Both lists and maps support bracket indexing as an alternative to item X of:

Both compile to the same code—use whichever reads better in context.

Sets

Sets store unique elements with no duplicates. Unlike lists, sets have no order and no index.

Create a set:

Let numbers be a new Set of Int.

Add elements:

Add 5 to numbers.

Remove elements:

Remove 5 from numbers.

Check membership:

If numbers contains 5: or If 5 in numbers:

Set operations:

• a union b — elements in either set
• a intersection b — elements in both sets

Tuples

Tuples are fixed-size collections that can hold values of different types. Unlike lists, tuples can mix integers, text, and other types in a single collection.

Create a tuple:

Let point be (10, 20).

Let record be ("Alice", 25, true).

Access elements (1-indexed):

Let x be point[1]. or Let x be item 1 of point.

Get length:

Let size be length of record.

Tuples are useful for returning multiple values from functions or grouping related but differently-typed data without defining a struct.

Beyond primitive types and collections, LOGOS lets you define your own types to model your problem domain.

Structs

A struct (structure) groups related values together. Define one in a ## Definition block using A [TypeName] has: syntax.

Creating Instances

Use a new [Type] with [fields] to create instances.

Accessing Fields

Use 's (possessive) to access fields.

Enums

An enum (enumeration) defines a type that can be one of several variants using A [TypeName] is either: syntax.

Pattern Matching

Use Inspect to handle different enum variants with When clauses.

Generics let you write types and functions that work with any type, not only specific ones.

Generic Types

Define a generic type with [T] in the type name. The [T] is a placeholder that gets replaced with a real type when you use it.

Multiple Type Parameters

You can have multiple type parameters like [A] and [B].

Generic Collections

Collections are generic types. Seq of Int is a sequence of integers.

Nested Generics

You can nest generic types like Seq of (Seq of Int) for a matrix.

Mental model: Box of [T] is a labeled shipping container: [T] is the blank
on the label. Stamp it — Box of Int — and the checker refuses mismatched cargo at
the dock. The label exists for the checker alone: by the time the program runs,
there is no label left, only the value that passed inspection.

LOGOS uses Socratic error messages—friendly, educational feedback that teaches while it corrects.

The Philosophy

Instead of cryptic compiler errors, LOGOS explains:

• What went wrong
• Where it happened
• Why it's a problem
• How to fix it

Modeling Failure

Model success and failure as an enum and pattern-match on it — the Outcome example below shows

the whole pattern. The standard library's generic Result works exactly the same way: construct

with a new Ok with value x / a new Err with error msg, match with When Ok (v): /

When Err (e):. And for "maybe a value": some x and none build an Option you can

Inspect with When Some (v): / When None:.

Error Propagation

Errors propagate naturally through return values. Handle them where appropriate.

Defensive Programming

Use assertions and guards to prevent errors before they happen.

Ten sections of core language deserve proof of mastery. The four challenges below

each blend two or more sections — none can be solved by pattern-matching a single

example, and one reaches back to Part I on purpose.

If a challenge stumps you, its hints name the moves; the section to reread follows

from them.

LOGOS provides memory safety through an ownership system expressed in natural English. Instead of cryptic symbols, you use verbs that describe what you're doing with data.

The Three Verbs

Ownership Rules

• Single Owner: Every value has exactly one owner at a time
• Move Semantics: Give transfers ownership—you can't use it after
• Borrow Checking: References (Show) can't outlive the owner
• Exclusive Mutation: Only one Let modify at a time

Common Patterns

• Copy first, then give
• Show multiple times (all OK — reads never conflict)
• Sequential mutation

The copy of Expression

Use copy of to create a deep clone of a value. This lets you keep using the original while giving away the copy.

Mental model: A value is a physical object. Give hands it over — your hand is
empty afterwards, and the compiler says so if you forget. Show x to f holds the
object up to the glass: f looks, nobody keeps. copy of runs the photocopier first.
The analogy's limit: copies are honest duplicates, not originals — changing one
never touches the other.

For high-performance scenarios, LOGOS provides Zones—memory regions where allocations are fast and cleanup is instant.

Why Zones?

The Hotel California Rule

"What happens in the Zone, stays in the Zone."

References to zone-allocated data cannot escape. To get data out of a zone, make an explicit copy.

Zone Configuration

Default size: 4 KB (4096 bytes) when not specified.

Specifying size: Use of size with units:

Zone Types

When to Use Zones

Use zones when:

• Processing large amounts of temporary data
• Performance is critical (games, simulations)
• Memory allocation patterns are predictable
• You want instant cleanup

Mental model: The zone is a whiteboard room: allocate by writing anywhere on the
board, free by erasing the whole board on the way out — one wipe, no matter how much
was written. What happens in the zone stays in the zone: to keep a result, copy it
out before the wipe. The board is not magic memory — oversized data needs a bigger
board, asked for with of size.

Word8, Word16, Word32, and Word64 are fixed-width machine words: arithmetic on

them wraps (the ring ℤ/2ⁿ) instead of promoting. That is not a limitation — it is the

substrate hashing, checksums, and ciphers are built on. The LOGOS standard library's

SHA-3, ChaCha20, and ML-KEM are written in LOGOS itself on exactly these words.

The word vocabulary

Wrapping is the point

word32(4294967295) + word32(1) is exactly 0 — the carry falls off the 32nd bit. Name

the behavior and it becomes a tool: rotation, mixing, and diffusion in ciphers all depend

on it.

Plain Int bit tools

Int has bit operations too: shifted left by / shifted right by, xor, and

count_ones(n) (the number of set bits).

Mental model: A word is a car odometer with a fixed number of digits: 99999 + 1
rolls to 00000 — the roll-over is the mechanism, not a malfunction. Rotation spins the
digits around the dial without losing any. The odometer's limit: it counts patterns,
not meaning — words are raw bit patterns; what they stand for is yours to assign.

*Try it: in the xorshift example, run twice — same seed, same output, every time. Change

the seed and watch the whole sequence change.*

LOGOS provides safe concurrency through structured patterns. No data races, no deadlocks.

Concurrent Patterns Overview

Attempt All (Async I/O)

Use Attempt all of the following: for I/O operations that wait on external resources. All operations run concurrently, and the program waits until all complete.

Variables declared in concurrent blocks are captured and returned as a tuple.

Simultaneously (Parallel CPU)

Use Simultaneously: for CPU-intensive work. Computations run in parallel on different CPU cores.

• 2 tasks → uses rayon::join (work-stealing thread pool)
• 3+ tasks → uses std::thread::spawn (dedicated threads)

Tasks (Green Threads)

Use Launch a task to... to spawn a green thread that runs concurrently. For fire-and-forget work, launch and move on:

Launch a task to process(data).

To control the task later (cancel, await), capture a handle:

Let worker be Launch a task to process(data).

Stop a running task with:

Stop worker.

Channels (Pipes)

Pipes are Go-style channels for message passing between tasks.

Create a channel:

Let jobs be a new Pipe of Int.

Send into a channel (blocking):

Send value into jobs.

Receive from a channel (blocking):

Receive item from jobs.

Non-blocking variants:

Try to send value into jobs.

Try to receive item from jobs.

Select (Racing Operations)

Use Await the first of: to race multiple operations. The first one to complete wins:

Await the first of:
    Receive msg from inbox:
        Show msg.
    After 5 seconds:
        Show "timeout".

Branch types:

• Receive var from pipe: — wait for channel message
• After N seconds: — timeout branch

Ownership and Concurrency

The ownership system prevents data races. Multiple reads are OK, but concurrent writes are prevented.

Note: Everything above — tasks, pipes, and select — runs right here in the browser playground on the deterministic scheduler. Compiled programs run the same code on the real multi-threaded runtime.

Deterministic replay

A concurrent LOGOS run is a pure function of the program and a seed: the scheduler's every

choice derives from LOGOS_SEED, so a race you saw once is a race you can replay forever —

same seed, same interleaving, byte-identical output. Concurrency bugs stop being

heisenbugs.

Mental model: Tasks are relay runners; pipes are the baton-passing lanes between
them. The scheduler is a referee working from a script: every "who runs next" choice
is written by the seed, so re-running the race replays every hand-off exactly. The
script covers scheduling only — a wrong program replays its wrongness deterministically.

When you need to reach outside the language, three doors open — all in compiled programs.

Escape to Rust

An Escape to Rust: block embeds raw Rust in place; largo build compiles it into the

binary as-is. The playground shows the honest boundary: it cannot interpret raw Rust, and

says so.

Native functions

## To native <name> (…) -> <Type> declares a function whose body is provided by the

host — the mechanism behind the standard library's now, read, and randomInt.

Exporting to WASM

Mark a function is exported for wasm and largo build --emit wasm produces a module

whose exports call straight into your LOGOS code — no JavaScript shims, no rustc in the

loop. The decorator parses and runs everywhere — it *matters* at largo build --emit wasm.

Ownership, zones, machine words, concurrency — the systems toolkit. Three challenges

below blend them, and one reaches back to Part II on purpose. The recall cards then

collect on the part's promises.

What are CRDTs?

CRDTs (Conflict-free Replicated Data Types) are data structures that can be replicated across multiple computers and merged without coordination. No matter what order updates arrive, the final state converges to the same result.

Why CRDTs Matter

Shared Structs

Mark a struct as Shared to enable automatic merge support. The compiler generates a merge method that combines two instances.

Built-in CRDT Types

ConvergentCount

A grow-only counter (G-Counter). Multiple replicas can increment independently, and when merged, the total reflects all increments. Useful for view counts, likes, or any monotonically increasing metric.

Tally

A bidirectional counter (PN-Counter) that supports both increment and decrement. Unlike ConvergentCount, values can go up and down—even negative. Useful for scores, balances, and temperatures.

LastWriteWins

A register that resolves conflicts by timestamp. The most recent write wins. Works with any type: Text, Int, Bool, etc.

Divergent

A multi-value register that preserves all concurrent writes instead of silently picking a winner. When replicas write different values concurrently, both are kept until you explicitly Resolve the conflict. Useful for collaborative editing where conflicts should be visible.

SharedSet

An observed-remove set (OR-Set) that supports both adding and removing elements. By default uses add-wins semantics: if one replica adds while another removes, the element stays.

Configuring bias:

• SharedSet (AddWins) of T — concurrent add beats remove (default)
• SharedSet (RemoveWins) of T — concurrent remove beats add

SharedSequence

An ordered CRDT list using the RGA (Replicated Growable Array) algorithm. Elements maintain their order across replicas. Useful for ordered lists, chat history, and document lines.

CollaborativeSequence

A text-optimized sequence using the YATA algorithm. Better conflict resolution for concurrent insertions at the same position. Ideal for collaborative text editing. Alternative syntax: SharedSequence (YATA) of T.

SharedMap

A key-value CRDT map (OR-Map). Keys can be added and removed, and values are themselves CRDTs that merge recursively. Alternative syntax: ORMap from K to V.

Merge Operations

Use Merge source into target to combine two CRDT instances. The target is updated in place with the merged state.

Persistence

CRDTs can be persisted to disk using the Persistent type modifier and Mount statement. Data is stored in append-only journal files (.lsf format) with automatic compaction.

The Persistent Type:

Persistent Counter wraps a Shared struct with journaling. All mutations are durably recorded.

The Mount Statement:

Mount [variable] at [path].

or

Let x be mounted at "path/to/data.lsf".

This loads existing state from the journal file (if present) or creates a new one. Changes are automatically persisted.

Network Synchronization

CRDTs earn their keep when synchronized across the network. Use Sync to subscribe a variable to a GossipSub topic.

The Sync Statement:

Sync [variable] on [topic].

• variable — A mutable variable containing a Shared struct
• topic — A string or variable naming the GossipSub topic

What Sync Does:

• Subscribes to the topic for incoming messages
• Spawns a background task to merge incoming updates
• Broadcasts the full state after any mutation

Persistence + Network

For the best of both worlds, combine Persistent types with Sync. The Distributed runtime ensures:

• Local changes are journaled before broadcast
• Remote updates are merged and persisted
• Data survives restarts

Note: In the playground, Sync runs in local single-node mode — the statement executes, but there are no real peers to gossip with. Mount/Persistent journaling and SharedMap need the compiled runtime; those examples are marked "(Compiled Only)".

Mental model: Replicas are notebooks kept by different reporters: syncing is the
union of FACTS — increments, adds, timestamped writes — never a fight over one pen.
Convergence is guaranteed because a union doesn't care what order the facts arrive in.
The limit: union needs facts designed to union — a plain overwrite degenerates to
LastWriteWins, where the later clock wins and the earlier write is gone.

LOGOS includes built-in peer-to-peer networking primitives for building distributed applications.

Note: In the playground these examples run in offline single-node mode — Listen, Send, and mDNS setup execute locally with no real network. Connect and PeerAgent dial live peers, so they need a compiled program; those examples are marked "(Compiled Only)".

Core Concepts

Portable Types

Messages sent over the network must be Portable. Mark your struct with is Portable to enable network serialization.

Address Format

LOGOS uses libp2p multiaddresses:

Automatic Peer Discovery (mDNS)

When you Listen, LOGOS automatically enables mDNS (multicast DNS) for local network peer discovery. Peers on the same LAN will discover each other without manual configuration.

• Works on WiFi networks, local development
• No configuration required — Listen is enough
• Peers are auto-connected when discovered

GossipSub (Pub/Sub)

The Sync statement uses GossipSub, a pub/sub protocol for broadcasting messages to topic subscribers:

• Topics are strings (e.g., "game-scores", "player-data")
• When you mutate a synced variable, the full state broadcasts to all subscribers
• Incoming messages are automatically merged in the background
• Retry with exponential backoff: 1s, 2s, 4s, 8s, 16s

File Transfer

For large file transfers, LOGOS provides FileSipper—a chunked transfer protocol:

This enables resumable transfers over unreliable networks.

Building a P2P Application

• Define Portable message types
• Listen on an address (server)
• Connect to peers (client)
• Create PeerAgent handles
• Send messages
• Use Sync for automatic CRDT replication

Security in Natural Language

LOGOS lets you express security policies as natural English sentences. These compile into efficient runtime checks that can never be optimized away.

Policy Blocks

Define security rules in ## Policy blocks. Policies define predicates (conditions on a single entity) and capabilities (permissions involving multiple entities).

Predicates

A predicate is a boolean condition on a subject:

A User is admin if the user's role equals "admin".

This generates a method is_admin() on the User type.

Capabilities

A capability defines what a subject can do with an object:

A User can publish the Document if the user is admin.

This generates a method can_publish(&Document) on the User type.

Check Statements

Use Check to enforce security at runtime. Unlike Assert, Check statements are mandatory and can never be optimized away.

Policy Composition

Policies can use AND and OR to combine conditions, and can reference other predicates.

CRDTs, networking, and policies close the distributed story. Three challenges blend

them — two reach back to earlier parts on purpose — and the recall cards collect on

the part's promises.

Organize large programs across multiple files using the module system.

Importing Modules

Use Use to import a module.

Qualified Access

Access module contents with the possessive 's.

Creating Modules

Each .md file is a module. The filename becomes the module name.

Visibility

By default, all definitions are public. Mark fields private with no public modifier.

The playground runs single-file programs, so the example below shows the module SHAPE

in one file — definitions above, ## Main below. Multi-file Use imports are a

largo-project feature.

LOGOS projects are built with largo, the LOGOS build tool.

Installing

curl -fsSL https://logicaffeine.com/install.sh | sh

Windows: powershell -ExecutionPolicy Bypass -c "irm https://logicaffeine.com/install.ps1 | iex".

Prebuilt for Linux/macOS (x64 + arm64) and Windows x64, SHA-256-verified, installed to

~/.local/bin with no sudo. --full bundles Z3 static verification.

Creating a Project

This creates a Largo.toml manifest and src/main.lg entry point.

Build Commands

The Wider Verbs

Package Registry

Publish and manage packages on the LOGOS registry:

Project Manifest

The Largo.toml file defines package metadata and dependencies:

[package]
name = "myproject"
version = "0.1.0"
entry = "src/main.lg"

[dependencies]

LOGOS provides built-in functions for common operations.

Currently Available

These built-ins work in both the playground and compiled programs:

• Show x. — Output values to the console
• length of x — Get the length of a list or text
• format(x) — Convert any value to text
• abs(n) — Absolute value of a number
• min(a, b) — Minimum of two integers
• max(a, b) — Maximum of two integers

Standard Library Modules

These modules import themselves the moment you call them — no Use line needed:

Every stdlib definition carries literate ## Note documentation — hover over a call in the

editor, or run largo doc, to read it.

File, environment, and network access follow the host program: compiled programs get the real

operating system, while the browser playground is sandboxed, so those calls are limited here.

One program, five ways to execute it — you choose the tradeoff, the semantics never change:

Translation validation proves the compiled tiers faithful: the emitted Rust is checked

equivalent to the source semantics with an SMT solver — you do not have to trust the

compiler, you can check it.

Steering the optimizer

## No <Name> decorators disable a named optimization for the program (forty exist —

Memo, Tco, Inline, Unroll, …), and ## Tier opt pins the VM's tier-up policy.

Both parse and run everywhere; they *matter* to the compiled tiers. largo opts <file>

reports which optimizations actually fired.

Mental model: One recipe, five kitchens: a tasting counter (interpreter), a prep
line (VM), a flash grill (JIT), a full restaurant build (AOT Rust), and a food truck
(direct WASM). Same dish every time — translation validation is the taste test that
proves the plating identical. Only the speed changes; the menu never does.

*Try it: both examples below print the same 42 — the decorators change how it runs, never

what it means.*

Modules, largo, the stdlib, and the five tiers — the working-programmer's toolkit.

Three challenges blend them with earlier parts, then the recall cards collect.

LOGOS can translate English sentences into First-Order Logic (FOL). This is useful for formal verification, knowledge representation, and understanding the logical structure of natural language.

Quantifiers

Connectives

Modals

Tense and Aspect

• PAST(P) — past tense
• FUT(P) — future tense
• PROG(P) — progressive aspect
• PERF(P) — perfect aspect

Mental model: Every verb is an EVENT with name tags on its participants:
"John runs" becomes ∃e(Run(e) ∧ Agent(e, John)) — there exists a running, and John
is its agent. Adverbs decorate the event, tense stamps it, roles name who did what
to whom. The limit: pure states (being tall) ride the same machinery — linguists
argue about that; the parser commits.

LOGOS bridges imperative programming with formal verification through assertions and proof statements.

Assert

Use Assert to verify conditions at runtime. If an assertion fails, the program stops with a clear error message.

Trust with Justification

Use Trust for conditions the compiler can't verify automatically. The because clause is mandatory—it documents your reasoning.

Trust Generates Debug Assertions

In development builds, Trust becomes a debug_assert!. In release builds, it generates no code—the trust is assumed.

Auditing Trust Statements

Every Trust stays a plain Trust that ... because ... line in your source—search for Trust that to review every assumption, each carrying the because justification that documents why it holds.

Proof Blocks (Advanced)

For formal verification, use theorem blocks with proofs documented in comments.

LOGOS can use the Z3 SMT solver to verify refinement types at compile time.

What is Z3?

Z3 is a theorem prover. Instead of checking constraints at runtime, Z3 proves (or disproves) them at compile time.

Variable Tracking

Z3 tracks constraints through variable assignments.

Compound Predicates

Multiple constraints can be combined.

Function Preconditions

Z3 verifies function contracts.

Enabling Z3 Verification

Enable with largo build --verify or in Largo.toml.

What Z3 Can Prove

In the playground, refinements are CARRIED, not checked — the proof happens at

largo build --verify. The second example below violates its own refinement on

purpose: predict what the playground does with it before you run it.

A ## Theorem block states premises and a goal in plain English; the proof engine finds

the derivation and the CoC kernel certifies it — not merely claims it. Run the example

below and the proof happens live, right here. The classic:

## Theorem: Socrates_Is_Mortal
Given: All men are mortal.
Given: Socrates is a man.
Prove: Socrates is mortal.
Proof: By automation.

$ largo prove syllogism.lg
Proved: Socrates_Is_Mortal — kernel-certified.

## Axiom and ## Theory blocks build larger developments — whole formal theories stated

in source text — and largo sat exposes the certified SAT solver directly (DIMACS in,

DRAT proofs out).

Mental model: The kernel is a referee, not a player: the proof engine searches
for the derivation, the kernel only CHECKS it, step by minimal step. A bug in the
search wastes time; only a bug in the tiny referee could certify a falsehood — which
is exactly why the referee stays tiny. The limit: "Not proved" means the search
failed, never that the statement is false.

Logic mode, assertions, refinements, proofs — the trust ladder from runtime guards to

kernel-certified theorems. Three challenges blend the rungs with earlier parts.

Complete programs, each read the way a problem is actually solved — Polya's four moves:

UNDERSTAND the problem (what exactly should print?), PLAN (which sections supply the

tools?), CARRY OUT (the build), and LOOK BACK (what generalizes, what breaks, what to

try next).

Warm-ups: Factorial, Fibonacci, Filtering

Three classics to loosen up on — recursion, recursion + a loop, and the

iterate–guard–accumulate shape you will use weekly.

Word Count

*Understand:* given words, print each distinct word with its count, first-seen order.

*Plan:* a Map for counts (Collections), a membership guard (Control Flow), destructured

iteration to report (Collections).

Look back: the count-by-key shape generalizes to any tally — errors by type,
sales by region. What breaks if the input is empty? Nothing: zero loop turns, zero
report lines. Try counting characters instead of words.

A Tiny Ledger

*Understand:* entries with labels and amounts; print each, then the total, in cents.

*Plan:* a struct for the entry (User-Defined Types), a typed empty list plus Push

(Collections), a running total (Control Flow), interpolation to report (Text).

Look back: amounts stay integer cents to dodge float dust — the same discipline
Money automates. What breaks with a negative amount? Nothing mechanical — but should
a ledger allow it? Try a credit/debit enum per entry.

A Todo List

*Understand:* seed tasks, add one, list all, then finish (pop) the newest.

*Plan:* list literals and Push/Pop (Collections), counted report via interpolation (Text).

Look back: Pop takes the NEWEST — a stack. For first-in-first-out, a Pipe
(Concurrency) is the queue shape. Try printing the remaining count after the pop.

Goal-indexed answers — each recipe is a complete program you can run and adapt. More

recipes land with every release; if a "how do I…?" you need is missing, that is a bug in

this guide.

• Format a number to two decimals — a format spec in the interpolation braces.

Combines: Text (format specs).

• Keep a value in range (clamp) — min and max compose.

Combines: the Standard Library (min/max) + Functions.

• Count matching items — iterate, guard with If, accumulate.

Combines: Control Flow + Collections + Text (interpolation).

Look back: every recipe is a shape, not a snippet — clamp works on any ordered
values, count-matching on any predicate. When you adapt one, change the domain first
and the shape last.

Syntax Cheat Sheet

Variables:

• Let x be 5. — Create variable
• Set x to 10. — Change variable
• Let x: Int be 5. — With type annotation

Control Flow:

• If condition: ... Otherwise: — Conditional
• While condition: — While loop
• Repeat for item in items: — For-each loop
• Return value. — Return from function

Functions:

• ## To name (param: Type) -> ReturnType: — Define function

Structs:

• A TypeName has: ... — Define struct
• Let x be a new TypeName with field1 value1. — Create instance
• x's field — Access field

Enums:

• A TypeName is either: ... — Define enum
• Inspect x: When Variant: ... — Pattern match

Primitive Types:

Lists (Seq):

• [1, 2, 3] — List literal
• item 1 of items or items[1] — Access (1-indexed)
• Push value to items. — Add to end
• length of items — Get length

Maps:

• Map of K to V — Map type (key-value pairs)
• a new Map of Text to Int — Create empty map
• item "key" of map or map["key"] — Get value by key
• Set item "key" of map to val. or Set map["key"] to val. — Set value

Sets:

• Set of T — Set type (unique elements)
• a new Set of Int — Create empty set
• Add x to set. — Add element
• Remove x from set. — Remove element
• set contains x — Check membership
• a union b — Elements in either set
• a intersection b — Elements in both sets

Tuples:

• (1, "two", 3.0) — Tuple literal (mixed types allowed)
• t[1] or item 1 of t — Access (1-indexed)
• length of t — Get tuple size

Ownership Verbs

Zones

Basic syntax:

• Inside a zone called "Name": — 4KB default zone
• Inside a zone called "Name" of size 2 MB: — Sized heap zone
• Inside a zone called "Name" mapped from "file.bin": — Memory-mapped file

Size units: B, KB, MB, GB

Concurrency

Async I/O:

• Attempt all of the following: — Concurrent async tasks (tokio::join!)

Parallel CPU:

• Simultaneously: — Parallel computation (rayon/threads)

Tasks:

• Launch a task to f(args). — Fire-and-forget spawn
• Let h be Launch a task to f(args). — Spawn with handle
• Stop h. — Abort a running task

Channels/Pipes:

• Let p be a new Pipe of Int. — Create bounded channel
• Send x into p. — Blocking send
• Receive x from p. — Blocking receive
• Try to send/receive — Non-blocking variants

Select:

• Await the first of: — Race multiple operations
• Receive x from p: — Channel receive branch
• After N seconds: — Timeout branch

Distributed Types (CRDTs)

Shared Structs:

• A Counter is Shared and has: — CRDT-enabled struct

CRDT Field Types:

• ConvergentCount — Grow-only counter (Increase)
• Tally — Bidirectional counter (Increase, Decrease)
• LastWriteWins of T — Timestamp-based register (Set)
• Divergent T — Multi-value register (Set, Resolve)
• SharedSet of T — Add/remove set (Add, Remove, contains)
• SharedSet (AddWins) of T — Set where add wins conflicts
• SharedSet (RemoveWins) of T — Set where remove wins conflicts
• SharedSequence of T — Ordered list RGA (Append)
• CollaborativeSequence of T — Text-optimized YATA (Append)
• SharedSequence (YATA) of T — Alternate YATA syntax
• SharedMap from K to V — Key-value CRDT ([] access)
• ORMap from K to V — Alternate map syntax

CRDT Operations:

• Increase x's field by amount. — Increment counter
• Decrease x's field by amount. — Decrement Tally
• Set x's field to value. — Set register value
• Resolve x's field to value. — Resolve Divergent conflict
• Add value to x's field. — Add to SharedSet
• Remove value from x's field. — Remove from SharedSet
• Append value to x's field. — Append to sequence
• Merge source into target. — Combine two CRDT instances

Persistence (Compiled Only):

• Persistent Counter — Type with automatic journaling
• Let x be mounted at "data.lsf". — Load/create persistent CRDT
• Mount x at "path". — Mount statement for persistence

Network Sync:

• Sync mutable_var on "topic". — Subscribe to GossipSub topic for auto-sync (real peers when compiled; local single-node mode in the playground)

P2P Networking

Server/Client:

• Listen on "/ip4/0.0.0.0/tcp/8000". — Bind to address
• Listen on "/ip4/0.0.0.0/tcp/0". — Listen on any available port
• Connect to addr. — Dial a peer
• Let remote be a PeerAgent at addr. — Create remote handle
• Send msg to remote. — Transmit message

Portable Types:

• A Message is Portable and has: — Network-serializable struct

Automatic Discovery:

• mDNS auto-discovers peers on local network when you Listen
• Peers are automatically connected when discovered

GossipSub (via Sync):

• Topics broadcast state changes to all subscribers
• Retry with exponential backoff (1s, 2s, 4s, 8s, 16s)

File Transfer:

• FileSipper for chunked transfers (1 MB chunks)
• FileManifest with SHA256 hashes for verification
• Enables resumable transfers

Security

Policy Blocks:

• ## Policy — Define security rules
• A User is admin if... — Define a predicate
• A User can edit the Doc if... — Define a capability

Security Enforcement:

• Check that user is admin. — Mandatory runtime check (never optimized out)
• Assert that x > 0. — Debug-only assertion (can be optimized out)

Logic Mode Symbols

The complete operator vocabulary — every English form and its symbolic twin. Neither

spelling is more "real"; they compile identically.

LOGOS errors teach — each states what happened, why it matters, and what to do. These

examples fail on purpose so you can read the real messages; the test suite locks

every displayed diagnostic word-for-word, so this gallery can never drift from the

compiler.

*Try it: run each one, read the message, then fix the program and watch it pass.*

Every example in this guide carries a truth badge: it either runs right here in the

browser playground, or it says exactly why it cannot. The badge, the Run button, and the

test suite all read the same declaration — and the suite executes every example on every

change, in both directions: a playground example that stops running fails the build, and

a compiled-only example that *starts* running fails the build too, until it is promoted.

This table is the complete list of examples that need the compiled runtime. Everything

not listed here runs in the playground.

To run one: copy the code into a largo new project and largo run.