Our mission: compile the universe's information. Not collect — compile, like code.

Try LOGOS online →

Logicaffeine is a natural-language compiler. You write English; it emits a formal artifact. It has two modes, sharing one parser:

The programming language is called LOGOS.

Imperative mode — English → Rust:

## To classify (n: Int) -> Text:
    If n is less than 0:
        Return "negative".
    Return "non-negative".

↓

#[inline]
fn classify(n: i64) -> String {
    if (n < 0) {
        return String::from("negative");
    }
    return String::from("non-negative");
}

That is the actual generated code — LOGOS even emits optimization hints like #[inline] itself.

Logic mode — English → First-Order Logic:

"Every man is mortal."   →   ∀x((Man(x) → Mortal(x)))

Why not just ask an LLM? LLMs are probabilistic — they guess. LOGOS is deterministic — it parses. When "every woman loves a man" has two readings, a model picks one; LOGOS returns both.

Early access. LOGOS is well-tested but the language surface is still stabilizing and subject to change. Please file bugs and feature requests via GitHub issues.

• Quick start
• A complete example: merge sort
• What's inside — the feature pillars
• Benchmarks — measured, not asserted
• Workspace map — the crates
• Documentation — the guides
• Project — roadmap, changelog, contributing, license

One line, no toolchain (Linux and macOS, x64 + arm64):

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

Windows:

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

That installs largo, the LOGOS build tool. Add --full (sh -s -- --full) for the build with Z3 static verification bundled. Every download is SHA-256-verified against the release's SHA256SUMS; nothing runs as root and no shell config is edited. Prefer cargo? cargo install logicaffeine-cli works too.

largo new hello && cd hello && largo run     # compile to native and run
largo repl                                    # the interactive session
largo logic "Every woman loves a man."        # English → ∀x(woman(x) → ∃y(man(y) ∧ love(x,y)))

No install required — open the Studio playground at logicaffeine.com/studio →. The full engine (parser, interpreter, proof engine, code generation) runs client-side in WebAssembly.

# Build the workspace
cargo build

# Run the tests (skips slow e2e; no Z3 toolchain needed)
cargo test -- --skip e2e

# Launch the web IDE — run from the repo root, not the app dir
dx serve -p logicaffeine-web

# Build the largo CLI, then scaffold and run a project
cargo build -p logicaffeine-cli
./target/debug/largo new my_project && cd my_project && ../target/debug/largo run

// Logic mode: English → First-Order Logic
let fol = logicaffeine_language::compile("Every man is mortal.")?;
// → "∀x((Man(x) → Mortal(x)))"

// Imperative mode: English → a self-contained Rust module
let rust = logicaffeine_compile::compile_to_rust("## Main\nReturn 42.")?;
// → a module that runs `Main` on a large-stack worker thread

Both return Result<String, ParseError>. See logicaffeine_language and logicaffeine_compile.

A full recursive algorithm — functions, typed collections, 1-indexed inclusive slicing, ownership (copy of), and control flow — written entirely in English. This program compiles and runs (grand_challenge_mergesort.rs):

## To Merge (left: Seq of Int) and (right: Seq of Int) -> Seq of Int:
    Let result be a new Seq of Int.
    Let i be 1.
    Let j be 1.
    Let n_left be length of left.
    Let n_right be length of right.

    While i is at most n_left and j is at most n_right:
        Let l_val be item i of left.
        Let r_val be item j of right.
        If l_val is less than r_val:
            Push l_val to result.
            Set i to i + 1.
        Otherwise:
            Push r_val to result.
            Set j to j + 1.

    While i is at most n_left:
        Let v be item i of left.
        Push v to result.
        Set i to i + 1.
    While j is at most n_right:
        Let v be item j of right.
        Push v to result.
        Set j to j + 1.

    Return result.

## To MergeSort (items: Seq of Int) -> Seq of Int:
    Let n be length of items.
    If n is less than 2:
        Return copy of items.
    Let mid be n / 2.
    Let left_slice be items 1 through mid.
    Let right_slice be items (mid + 1) through n.
    Let sorted_left be MergeSort(copy of left_slice).
    Let sorted_right be MergeSort(copy of right_slice).
    Return Merge(sorted_left, sorted_right).

## Main
    Let numbers be a new Seq of Int.
    Push 3 to numbers. Push 1 to numbers. Push 4 to numbers.
    Push 1 to numbers. Push 5 to numbers.
    Let sorted be MergeSort(numbers).
    Show sorted.

→ the imperative-mode guide covers each construct in depth.

Eight pillars. Each blurb links to a deeper, code-grounded guide.

A statically-typed language: variables and mutation, a rich primitive set (Int, Nat, Real, Rational, Bool, Text, Uuid, machine words Word8–Word64), user structs, sum-type enums, generics, closures, 1-indexed collections with inclusive slices, pattern matching, ownership/borrow checking, and FFI. → docs/imperative-mode.md

English → First-Order Logic with deep linguistic coverage: quantifiers, modal logic (Kripke semantics), tense/aspect and LTL, neo-Davidsonian event semantics, scope ambiguity enumeration, λ-calculus/Montague types, and a long tail of phenomena (presupposition, ellipsis, counterfactuals, binding…). → docs/logic-mode.md

One front-end, many back-ends: a tree-walking interpreter, a register bytecode VM, EXODIA — a copy-and-patch JIT (native), AOT Rust codegen, and a direct WASM backend (largo build --emit wasm, no rustc in the loop) — plus an experimental AOT C emitter. All benchmarked against C and V8. → docs/execution-and-performance.md

A pure Calculus-of-Constructions kernel with decision procedures (ring/lia/cc/omega), a backward-chaining proof engine with Socratic hints, optional Z3 static verification, and translation validation that proves the emitted Rust matches the source. → docs/proof-and-verification.md

Structured concurrency, channels and Select, agents/message-passing, 8 CRDT types, a deterministic (seed-replayable) scheduler, and networking via libp2p mesh + a thin WebSocket relay. → docs/concurrency.md

The stdlib's crypto layer is LOGOS source, not FFI: post-quantum ML-KEM-768, ChaCha20, and RFC 9562 UUIDs — every version, with the MD5 and SHA-1 digests implemented in LOGOS in uuid.lg — built on Word8–Word64 and SIMD lane types. ML-DSA-65 signing and the full Keccak/SHA-3 sponge are written in LOGOS in the test corpus, all bit-exact against FIPS and reference oracles on every execution tier. → docs/imperative-mode.md

A browser IDE (Logic / Code / Math / Hardware modes, streaming REPL, compile-to-Rust) and a gamified curriculum (four eras, SM-2 spaced repetition) — all running in WASM. → docs/studio-and-learn.md

A Cargo-style front door to the whole engine — 23 subcommands: projects (new/init/add/clean), build & run (build, run, check, emit rust|c|wasm, fmt, opts), logic & proof (logic, prove, sat, verify), the interactive repl, doc, doctor, and registry auth (publish/login/logout), driven by a Largo.toml manifest. → docs/cli.md

Measured, not asserted. The interactive suite lives at logicaffeine.com/benchmarks; the charts below are regenerated from benchmarks/results/ by gen-readme-charts.py.

How the execution tiers behind these numbers work → docs/execution-and-performance.md.

Crates are layered into dependency tiers and protected by four architectural invariants — Milner (kernel never sees the lexicon), Liskov (proof engine independent of the language), Lamport (data structures are IO-free and WASM-safe), and Tarski (verification IR is decoupled from the main AST). See docs/architecture.md for the full picture.

verify, tv, synth, and wirebench sit outside default-members — plain cargo build / cargo test need no Z3 toolchain; they build when the verification feature pulls them in.

Applications

Code-grounded guides live in docs/:

• Imperative mode — the LOGOS language
• Logic mode — English → First-Order Logic
• Execution & performance — interpreter, VM, JIT, AOT, direct WASM
• Proof & verification — kernel, proof engine, Z3, translation validation
• Concurrency & distributed — channels, agents, CRDTs, networking
• Studio & Learn — the web app
• The largo CLI — build tool & manifest
• Architecture — pipeline, tier graph, invariants

The test suite (crates/logicaffeine_tests/) is the living specification — features are organized into phase tests, with end-to-end differential tests proving the interpreter, VM, JIT, and AOT paths agree.

• Changelog — CHANGELOG.md
• Versioning policy — VERSIONING.md (lockstep SemVer across the workspace)
• Contributing — CONTRIBUTING.md
• Security — SECURITY.md
• License — Business Source License 1.1

"In the beginning was the Word, and the Word was with Logic, and the Word was Code."