Protoss docs

Install

macOS arm64 (other platforms: build from source, OCaml >= 5.1):

curl -fsSL https://store.protoss.app/releases/install.sh | sh

The installer verifies the tarball's sha256, unpacks binary + standard library to ~/.protoss/dist, and prints the PATH line for your shell. Update later by re-running the same line.

Five minutes

protoss init myapp
cd myapp
protoss live .        # http://localhost:8080/

You get a working full-stack counter: the local half lives in the page, the shared half lives in one backend model folded from an event log. Open two tabs, bump in one, watch the other move.

• Edit src/Frontend.protoss, save - the page reloads in ~0.6s. A failing save shows the type error in the page and keeps the last good build running.
• Press the hourglass button: the time-travel debugger. Click any past message to refold the app at that instant; present resumes.

The shape of an app

Three files. Types.protoss is the contract shared by both halves:

type alias FrontendModel =
    { count : Nat, shared : String }

type FrontendMsg
    = Bump
    | BumpShared
    | GotShared Nat

type ToBackend  = Bump
type ToFrontend = Synced Nat

Frontend.protoss - update is pure and synchronous (a click can never be lost or clobbered by a slow request); effects runs against the same (msg, model) pair and re-enters through normal dispatch:

update : FrontendMsg -> FrontendModel -> FrontendModel
update msg model =
    case msg of
        Bump _ -> { model | count = succ model.count }
        BumpShared _ -> model
        GotShared n -> { model | shared = Nat.toString n }

effects : FrontendMsg -> FrontendModel -> Process (Maybe FrontendMsg)
effects msg model =
    case msg of
        BumpShared _ ->
            bind (sendToBackend (Bump unit))
                (\m -> done (Some (GotShared m.count)))
        _ -> done None

view : FrontendModel -> View FrontendMsg
view model =
    column
        [ text (String.concat "local: " (Nat.toString model.count))
        , button "Bump local" (Bump unit)
        ]

Backend.protoss - the backend is not mutable state: it is the deterministic fold of updateBackend over the to-backend event log. Broadcasts push to every connected client; onConnect welcomes each new one:

updateBackend : ToBackend -> BackendModel -> Tuple BackendModel (Cmd {} ToFrontend)
updateBackend msg model =
    tuple { count = succ model.count } (broadcast (Synced (succ model.count)))

fromBackend : ToFrontend -> FrontendMsg
fromBackend tf =
    case tf of
        Synced n -> GotShared n

onConnect : BackendModel -> ToFrontend
onConnect model =
    Synced model.count

Language tour

The surface is deliberately Elm-like. Under it, every program canonicalizes to a typed graph and hashes to a stable p2: ref - two spellings of the same program get the same hash.

Types, records, unions

type alias User = { name : String, score : Nat }

type Shape
    = Circle Nat
    | Square Nat

area : Shape -> Nat
area s =
    case s of
        Circle r -> r * r * 3
        Square w -> w * w

Structural recursion

Protoss is total: every program terminates. Recursion is written the Elm way and checked structural - the recursive call must take the smaller part:

sum : List Nat -> Nat
sum xs =
    case xs of
        [] -> 0
        x :: rest -> x + sum rest

count : Nat -> Nat
count n =
    case n of
        0 -> 0
        succ m -> 1 + count m

Shapes the checker cannot prove terminating are rejected with the equivalent fold named in the error. Folds are also directly callable:

total : List Nat -> Nat
total xs =
    foldList xs 0 (\x acc -> x + acc)

Let, lambdas, prelude

describe : List Nat -> String
describe xs =
    let doubled = List.map xs (\x -> x * 2) in
    String.concat "n=" (Nat.toString (List.length doubled))

The standard library (List, Maybe, Result, Map, Set, String, Nat) is itself written in Protoss. Polymorphic functions apply directly: List.map, List.filter, List.reverse, ...

Effects and subscriptions

All effects are typed Process values built with done / bind; capabilities are declared per file (capabilities Server.request) and enforced by the checker.

Typed subscriptions (all optional defs; paused while time-traveling, replayed from the ledger):

onFrame   : Nat -> Model -> Maybe Msg      -- requestAnimationFrame, dt in ms
onKeyDown : String -> Model -> Maybe Msg
onKeyUp   : String -> Model -> Maybe Msg

Views are data (column, text, button, node/SVG...) - which is what makes a whole game run scrubbable: see the Game tab on protoss.app.

Deploy

With an invite token, your app goes live at <name>.protoss.app - no account, no infrastructure:

protoss deploy . --name <name> --token <your-invite-token>
# Deployed: https://<name>.protoss.app/

The backend runs at the edge as the same evaluator the browser runs, folding your updateBackend over a durable event log. Redeploying keeps the log: your data survives.

No invite yet? Ask the person who sent you here. Bring-your-own-Cloudflare is also supported: protoss deploy . --edge --domain yourdomain.com

CLI cheatsheet

Why Protoss

• Content-addressed: equivalent programs - any spelling, any machine - hash to the identical p2: ref. The store, packages and deploys are all derived from it; missing objects resolve from the world store automatically.
• Total and deterministic: no crashes, no non-termination, no wall-clock or randomness leaking into results. That is what makes replay exact.
• Time-travel is not a devtool bolt-on: the app is a fold over a message log, so any past state is recomputable - in dev AND in prod.
• One language, both halves: the browser and the edge run the same evaluator over the same typed contract. sendToBackend is typed end to end.
• Built for AI agents: programs are checked canonical graphs, and the MCP server mutates them only through validated patches - an agent can never leave the project in a broken state. See the For agents tab.