prometheus-lang 0.3.0

Prometheus: a capability-secure, deterministic-by-default programming language (bootstrap toolchain)

Prometheus

A programming language in which entire classes of software failure are unrepresentable.

Prometheus is designed around a small number of load-bearing ideas, each chosen because it deletes a category of bugs rather than merely discouraging it:

Failure class	Why it cannot happen in Prometheus
Memory corruption, dangling pointers, leaks	Pure value semantics: no observable aliasing, no manual memory, no null
Data races, deadlocks	No shared mutable state exists; par is deterministic by the confluence theorem for pure reductions
Hidden side effects, supply-chain "phone home"	Object-capability model: effects require an unforgeable capability value; a function's signature proves what it can touch
Missing-case bugs	Pattern matches are checked for totality at compile time
null / undefined	Option(a) is an ordinary library type; partial operations return it
Untested code paths	check — executable specifications — are a language construct, run by prom test, and double as documentation
Stale documentation	intent metadata is attached to definitions, machine-readable, and emitted by prom doc together with inferred types
Type annotation busywork	Full Hindley–Milner-style inference; annotations are optional and checked when present

Status: v0.3 "Hearth" (in progress). On top of the Kindling line (modules, Result, maps, capabilities, playground) v0.3 adds property-based checks and a language server (prom lsp). All implemented and tested. The design documents describe the full system; see Implementation status for the honest line between built and planned.

Try it without installing anything: the browser playground runs the real toolchain via WebAssembly (serve docs/ with GitHub Pages, or open locally with python3 -m http.server from the repo root and visit localhost:8000/docs/playground/).

Quickstart

No dependencies beyond Python ≥ 3.10:

$ ./prom run examples/hello.prom
Hello, world!

$ ./prom check examples/shapes.prom     # parse + infer + verify
area : (Shape) -> Float
total_area : (List(Shape)) -> Float
...

$ ./prom test examples/shapes.prom      # run executable specifications
checks: 3 passed, 0 failed

$ ./prom doc examples/shapes.prom       # docs from intents + inferred types
$ ./prom repl                           # interactive session

$ ./prom run examples/todo/main.prom add "learn prometheus"   # args + modules
added: learn prometheus

New to the language? Start with the tutorial, then the tour. VS Code highlighting lives in editors/vscode.

Thirty seconds of Prometheus

type Shape =
  Circle(Float)
  Rect(Float, Float)

intent "The area of a shape."
area(s: Shape): Float =
  match s                      # must cover every constructor — checked
    Circle(r) -> 3.14159 * r * r
    Rect(w, h) -> w * h

check area(Rect(3.0, 4.0)) == 12.0     # executable spec, run by `prom test`

main(io) =                     # io is a capability: the only key to the outside world
  par                          # deterministic parallelism — pure by construction
    a = total_area([Circle(1.0), Rect(2.0, 3.0)])
    b = sum(range(1, 1001))
  print(io, "area {a}, sum {b}")

total_area(shapes) =
  shapes |> map(area) |> fold(0.0, (acc, x) -> acc + x)

Things to notice:

• No annotation is required anywhere — total_area : (List(Shape)) -> Float is inferred. Annotations, when written, are verified claims, not instructions.
• main receives its authority. Nothing else in the program can perform I/O, because nothing else holds the io capability and capabilities are unforgeable (opaque types with no constructor).
• par cannot introduce a race. Its bindings must be pure; the runtime enforces it and the semantics are provably order-independent.
• The prelude is written in Prometheus (src/prom/stdlib/prelude.prom) and carries its own intents and checks — the standard library is its own specification and test suite.

Documentation

Document	Contents
docs/philosophy.md	Design principles, the bug-class elimination argument, honest scope
docs/tour.md	The whole language by example
docs/spec/grammar.md	Lexical structure and EBNF grammar (normative)
docs/spec/types.md	Type system: inference, soundness, capability types
docs/spec/semantics.md	Evaluation semantics; the determinism theorem for par
docs/capabilities-security.md	The security model
docs/memory-model.md	Value semantics now; the planned native memory strategy
docs/concurrency.md	From par to distributed dataflow
docs/compiler-architecture.md	Bootstrap internals and the native pipeline design
docs/ai-integration.md	Intent metadata, machine-readable diagnostics, the AI toolchain surface
docs/packages.md	Content-addressed package system design
docs/roadmap.md	Milestones from v0.1 to self-hosting
docs/tutorial.md	Guided build of a real program
CHANGELOG.md	Versions, breaking changes, migration notes
CONTRIBUTING.md	Ground rules and stability policy
editors/lsp.md	Editor setup for the language server

Repository layout

prom                  launcher (no install needed)
src/prom/             the bootstrap toolchain
  lexer.py            layout-aware lexer, string interpolation
  parser.py           recursive-descent parser
  types.py            HM-style inference, ADTs, records, totality checking
  eval.py             evaluator + capability runtime + par purity guard
  builtins.py         the minimal primitive layer under the prelude
  pipeline.py         source -> tokens -> AST -> types -> values
  cli.py              prom check | run | test | doc | repl
src/prom/stdlib/prelude.prom   the standard prelude, written in Prometheus
examples/             runnable, tested example programs (todo/ is multi-module)
tests/                89 unit + CLI + module tests
tools/                benchmarks and the playground builder
docs/                 design documents + browser playground
editors/vscode/       syntax highlighting extension

Implementation status

Implemented and tested today (bootstrap interpreter):

• layout syntax, string interpolation, pipelines (|>), lambdas, records
• algebraic data types with type parameters; total pattern matching
• Hindley–Milner-style inference with numeric defaulting and helpful diagnostics (source spans, carets, "did you mean", --json output)
• modules (use): qualified values, shared types/constructors, cross-file totality checking, cycle detection
• capability-gated effects (Io, Fs, Clock, Env, Net, Rand) — purity visible in types; main typed by grant name; args support
• Result-based error handling — fallible builtins return Result
• Map(k, v), text/parsing/sorting builtins, Pair/zip in the prelude
• deterministic par with runtime purity enforcement
• check executable specs (including property-based check for x: T: with shrinking) and intent metadata, doc generation, REPL
• language server (prom lsp): live diagnostics, hover types, outline
• browser playground running the real toolchain (Pyodide)

Designed, not yet implemented (see docs/roadmap.md for the plan and docs/philosophy.md for the honesty policy): property checks, formatter, LSP server, content-addressed packages, processes/channels, native code generation.

A note on the name: "Prometheus" collides with the ubiquitous monitoring system, which will hurt search discoverability if this goes wide. Renaming is cheap now and expensive later; the toolchain is isolated behind the prom command and one package name if a rename is chosen.

Development

$ cd tests && python3 -m unittest discover -p 'test_*.py'   # full suite
$ ./prom test src/prom/stdlib/prelude.prom                           # prelude self-checks
$ python3 tools/bench.py                                    # bootstrap benchmarks

Licensed under Apache-2.0.