Allegro

A programmable language platform where correctness is provable by construction.

Allegro is built around a thesis: code is not the artifact you should review — the semantic summary of the code is. Refinement types, lifecycle invariants, and function contracts accumulate facts the compiler can prove; the same facts surface in a single safety summary that humans (and AIs) review instead of reading line-by-line. Familiar syntax, an extensible grammar, and partial evaluation as the compilation model are the means; provability is the point.

Provability — the headline example

A small banking API demonstrates the four layers of Allegro's provability arc working together: a refinement type, arithmetic propagation, a function contract with requires and ensures, and runtime safety where static proof falls short.

The five layers, each with its own playable example. The first four are the positive aspect of provability — what the code does. The fifth is the negative aspect — what it doesn't do.

• Refinement types & domain propagation — facts attached to values flow through arithmetic.
• Asserts — universal in-scope predicates, discharged statically when the compiler can prove them.
• Lifecycle invariants — predicates that hold for every value of a type, checked on construction.
• Contracts — requires / ensures on functions, surfacing in the safety summary.
• Effects — what categories of side effects each function can produce; declared and verified against inference.

Refinement types & domain propagation

Constrain existing types with predicates using &&. The _ placeholder is the value. Construction and call-site checks fire automatically; the recognised algebraic shape (intervals, equality, inequality) propagates through arithmetic so downstream values inherit the proof.

Asserts

Activate use invariants for a universal assert statement. The predicate is checked against the binding's accumulated facts: if entailed, the runtime check disappears and the proven fact joins the binding's predicate set. If not, a runtime check fires and a failed assert halts visibly with a counterexample (no silent error values — build safety in).

Lifecycle invariants

Type.invariant(self => P) declares a predicate that holds for every value of the type. The constructor checks every clause; multi-clause chaining reports per-clause failure messages. Multi-field invariants reference fields via self.field.

Contracts: requires & ensures

Function bodies declare contracts at the head. requires P is a caller obligation; ensures P is an implementer guarantee, with _ referring to the return value. Predicate-set entailment short-circuits both runtime checks; the post-condition attaches to the result so callers see the proven fact.

Effects — the negative aspect

Each function can declare which categories of side effects it produces — io, net, time, … — via an effects body clause. The analyzer infers the actual set from the primitives transitively called and verifies the declaration is a superset (under-promising halts compilation). Click Inspect to see the inferred and declared sets surface in the safety summary.

Effect labels are extensible, not a fixed enum. Core ships only the implicit pure; the standard library registers io alongside print, net alongside fetch, and so on. Domain-specific extensions can register their own labels (build-io, funds-mutation, …).

Try editing the square function to add a print(x) call without removing effects pure — running halts with an effects-mismatch error pointing at the undeclared io effect.

Basics

Bindings, arithmetic, functions, and control flow. Allegro uses => for function definitions and if/then/else for conditionals.

Types

Every value in Allegro Standard has a type. Types enable dot-access dispatch, type checking, and compile-time inference. Built-in types include Int, Float, String, Bool, Array, and Object.

Pattern Matching

Pattern matching with when/is/then. Supports literals, wildcards, bindings, type destructuring, structural destructuring, nested patterns, and guard clauses.

Collections

Arrays support bracket access, map, filter, reduce, and chaining. Objects support dot access and destructuring.

Custom Types

Create types using the fluent API. extend creates record types, distinct creates newtypes. Types themselves are typed values — Int instanceof NominalType is true.

Interfaces

Interfaces declare required members using structural type matching. Any type with the right members satisfies the interface — no implements keyword needed.

Mixins

Add method implementations to types with .mixin(). Mixin methods receive self as their first argument and can access fields and call other methods.

Error Handling

Errors are values, not exceptions. They propagate automatically through operations. Use error of to inspect, and pattern matching to handle.

Implicit Async

Allegro handles async operations without await. Expressions that depend on unresolved futures automatically defer and re-evaluate when results arrive. print streams output as values become available.

Grammar Extensions

Allegro exposes its Earley parser as first-class primitives. Build a grammar at runtime, parse strings into trees of Allegro values, and interpret those trees in pure Allegro — build a DSL in a page of code.

The example below builds a minimal regex DSL: literal chars, | alternation, */+/? postfix. The grammar is defined with grammar_terminal, grammar_phrase, grammar_choice, grammar_repeat, grammar_optional. The parse tree is then interpreted by pure Allegro functions to produce a matcher.

Runtime Grammar

Beyond building standalone DSL grammars, Allegro lets modules extend the host language itself. Inside a grammar { … } block, a module declares new operators, keywords, or entire multi-token expressions. Files that opt in with a use NAME header get those syntactic additions before parsing starts.

Four operator-level declarations plus user rules and multi-token forms, all sharing one grammar block:

• infix S prec(X) left/right/none => (l, r) => ast — binary operator at a named precedence level
• prefix S at(X) => x => ast — unary prefix symbol (e.g. #x)
• postfix S at(X) => x => ast — unary postfix symbol (e.g. n!)
• expr_prefix KW => x => ast — keyword followed by one expression (e.g. neg x)
• rule NAME = ebnf => template — user sub-rule used by forms
• expr_form parts => template — multi-token inline expression (match x with …)
• stmt_form parts => template — multi-token statement form

Precedence is named, not numeric. Use at(mul) to place at an existing level, prec(pow) above(mul) below(unary) to declare a new level between existing ones, or at("*") to look up by operator symbol.

Here's lib/pow.alg — adds ** and neg:

pow_helper(base, n, acc) =>
  if n == 0 then acc else pow_helper(base, n - 1, acc * base)

pow_int(base, n) => pow_helper(base, n, 1)

pow_grammar = grammar {
  infix "**" prec(pow) above(mul) below(unary) right => (l, r) => pow_int(l, r)
  expr_prefix "neg" => x => 0 - x
}

A consumer file declares use pow at the top and uses the new syntax as if it were built in:

Multi-token forms let a single module ship a whole new expression shape. Here's lib/match_expr.alg — a match x with p => e | … form that desugars to a linear search:

match_helper(scrutinee, cases, idx) =>
  if idx == cases.length
    then error "match: no branch matched"
    else if scrutinee == cases[idx].p
      then cases[idx].e
      else match_helper(scrutinee, cases, idx + 1)

match_dispatch(scrutinee, cases) =>
  match_helper(scrutinee, cases, 0)

match_grammar = grammar {
  rule match_case = p:expr "=>" e:expr      => (p, e) => {p: p, e: e}
  rule match_list = c:match_case ** "|"      => c => c

  expr_form "match" s:expr "with" cs:match_list
    => (s, cs) => match_dispatch(s, cs)
}

EBNF inside a rule body: "literal", ident references, s:rule labels, a* / a+ / a? repetition, a ** sep separator-rep, (a | b) alternation. Templates receive labels as positional params.

The mechanism is module-scoped — only files that use-declare pow or match_expr see those additions. Cross-module conflicts (two modules registering the same operator, cyclic precedence declarations) surface at use time with aggregated error messages. Other files still parse as plain Allegro Standard.

More forms (Phase 7)

A few more ways to declare and activate grammars:

• new grammar { … } — fresh grammar, not an extension of Allegro. Used for standalone DSLs.
• grammar extends X { … } — build on any existing Grammar value, not just Allegro.
• use grammar { … } — declare a grammar inline at the top of a file, no separate module required.
• use NAME.MEMBER — select one specific Grammar binding from a module that exports several.
• rule foo += body => template — append an alternative to an existing production.
• rule foo[alt] = body => template — replace a single named alternative.
• rule foo -= alt — remove an alternative.

Templates are hygienically substituted: symbols inside a grammar block resolve against the module that declared the block, not the consumer's scope. A consumer that happens to rebind a name the template uses can't silently hijack the grammar extension.

Recursive Algorithms

Allegro supports tail call optimization. Write recursive algorithms naturally — they use O(1) stack space when in tail position.