ASL is a type-safe, effect-tracked programming language where uncertainty, taint, cost, and capability requirements are enforced at compile time — not patched on at runtime.
#[requires(cap::network_read, cap::inference)] agent Researcher { // All effects tracked in Computation<T, ε> fn analyse(query: String) -> Uncertain<Report> !{Network, Inference} { let raw: Computation<Data, ε> = perform Effect::NetworkFetch(query) requires cap::network_read; // Uncertainty + taint + cost + caps checked here discharge raw with { confidence: 0.80, taint: taint::Agnostic, budget: 5000, capabilities: [cap::inference], } { // inner value is plain Data — safe to use let result = infer<Report>( model: tier::cloud_mid, prompt: build_prompt(raw), budget: think::medium, ); result } } }
Where a new feature conflicts with a lower-numbered principle, the lower-numbered principle wins. No exceptions.
Uncertain<T> with a probability interval [lo, hi]. It cannot be silently discarded.
Introduces the Computation〈T,ε〉 graded monad and the discharge gate as the sole mechanism to unwrap effectful values. Presents a formal type system extending Hindley‑Milner with affine types, effect rows, and taint levels. Proves two safety theorems — effect soundness and taint integrity — and describes an end‑to‑end implementation with a 253‑test conformance suite.
perform is syntactically within a discharge block — proved by induction on typing derivations.perform without an intervening sanitize — enforced at both compile time and runtime.ASL formal specification — lexical grammar, complete EBNF syntax, the type system (Hindley‑Milner + affine types + effect rows + taint lattice), 8‑layer memory architecture, heartbeat/dream cycles, capability tokens, session protocols, temporal contracts, corrigibility, provenance chain, grammar stratification (S0‑S3), ISA extensions, the full standard library, and the ASL‑CONF‑15 conformance suite. Grounded in twenty‑one cited academic sources across effect systems, session types, capability security, taint tracking, stigmergy, and corrigibility.
The discharge block is the only way to unwrap a Computation<T,ε>. The compiler enforces this. The VM enforces it again.
ASL partitions its grammar into four strata. The compiler rejects any construct above the declared stratum level at parse time. Escalation requires a human principal countersignature — an agent cannot self-escalate.
Built into the language — not bolted on as a library or a runtime guard.
Computation<T,ε> carrying uncertainty interval, taint provenance, cost bounds, and held capabilities. The wrapper is opaque — you must discharge it.T. The VM validates model output against this schema before binding — schema mismatches surface as InferenceError, never silent garbage.perform expression must declare the required token. Capability checks are conjunctive across agent composition.cap::untyped_mesh.act.ProvenanceTag in an append-only DAG. Deterministic seedvm replay enables counterfactual surgery and full audit without trust in the agent itself.Existing frameworks apply safety policies as runtime guards bolted onto programs written in conventional languages. ASL makes safety a property of the type system itself.
| Property | ASL v0.1 | LangGraph / AutoGen | AgentSpec | Agent-C (LTL+SMT) |
|---|---|---|---|---|
| Effect tracking | ✓ compile-time | ✗ none | ~ runtime only | ✗ none |
| Uncertainty typing | ✓ Uncertain<T> enforced | ✗ discarded silently | ✗ not modelled | ✗ not modelled |
| Taint / information flow | ✓ three-level lattice | ✗ none | ✗ none | ✗ none |
| Capability security | ✓ unforgeable tokens | ✗ convention only | ~ predicate rules | ✗ none |
| Temporal contracts | ✓ LTL + SMT, S2+ | ✗ none | ~ trigger rules | ✓ LTL + SMT |
| Provenance / audit | ✓ Merkle DAG, replayable | ✗ informal | ~ trajectory log | ✗ none |
| Session-typed comms | ✓ deadlock-free at compile time | ✗ none | ✗ none | ✗ none |
| Enforcement layer | ✓ static + runtime (dual) | ✗ none | ~ runtime only | ~ runtime only |
| Applies to existing code | ✗ requires ASL | ✓ Python / JS | ✓ any framework | ✓ any framework |
✓ supported · ~ partial / runtime only · ✗ not supported. ASL's tradeoff: intrinsic guarantees require programs to be written in ASL.