Compile-Time Safety

Where to start

Recommended prior reading: Batteries-Included and Effect Contracts & Capability Discipline. This pillar is the most PL-theory-dense of the six — effect system, affine types, refinement types, taint analysis. Those preceding pillars introduce the effect vocabulary and the contract framing that make this content accessible. Hit an unfamiliar term? See the Glossary.

Compile-time safety is Arcana’s irreducible core. Every other pillar — effect contracts, batteries-included capabilities, the portable runtime, self-hosting, governance — rests on what the type system can statically prove before code runs.

The premise: side effects and resource discipline are enforced by the type system, not by convention. If a generator (human or AI) writes code that would violate a declared safety constraint, the compiler rejects it before the code reaches the runtime.

What the compiler enforces today

Effect system

Every function declares the side effects it performs. Effects are first-class citizens of the type system — they appear in function signatures, they propagate through call chains, and they’re drawn from a closed, governed vocabulary (effects are added, retired, or rejected through a documented process, not invented ad-hoc).

Below is get_post_by_id from tests/rpc-fixtures/blog.arcana — a verified fixture showing how an effect declared in the signature becomes the function’s contract. The {Database} effect row is the compiler’s promise about what this function is permitted to do.

Canonical (S-expression)

;; pub fn get_post_by_id(post_id: Int) -> {Database} Int
(dc-fn :fn
  (fn-decl
    :body (block
      :stmts ()
      :expr (ex-call
        :args (
          (arg-positional :expr (ex-lit :value (lit-string :value "SELECT id, title, body, published FROM posts WHERE id = ?")))
          (arg-positional :expr (ex-ident :name "post_id")))
        :fn (ex-ident :name "db_query_one")))
    :contracts ()
    :effects (Database)
    :name "get_post_by_id"
    :params (
      (param :modifier none :name "post_id" :type (ty-named :path "Int")))
    :ret (ty-named :path "Int")
    :tparams ()
    :vis pub))

Human view

pub fn get_post_by_id(post_id: Int) -> {Database} Int {
  db_query_one("SELECT id, title, body, published FROM posts WHERE id = ?", post_id)
}

The effect row {Database} makes the contract visible at signature-read time. A function with an empty effect row (pub fn add(a: Int, b: Int) -> Int { a + b }) is pure — calling an effectful function from a pure function is a compile error, because the declared effect row doesn’t admit the effect. This is what gives an evaluator — a human reader, an AI reviewer, a deployment manifest — confidence about what a unit of generated code is permitted to do without reading its body.

This is what gives an evaluator — a human reader, an AI reviewer, a deployment manifest — confidence about what a unit of generated code is permitted to do without reading its body. The effect row is the contract.

Affine resource types

A resource handle — a database connection, a file handle, an open HTTP response, an API session — must be consumed exactly once. Double-use of a resource handle is a compile error. Undeclared drop is a compile error. The check operates on Arcana-typed values and does not extend across Unsafe FFI boundaries or to native resources owned by the host runtime — those remain the host’s responsibility.

The affine discipline is best illustrated by a synthetic-violation test from the gate corpus: double_use from tests/v1.5-validation/1a_double_use.arcana. The fixture’s move parameter h is consumed twice in the same scope — the compiler refuses to emit the program and produces error code E6010 [AFFINE-USE-AFTER-MOVE].

Canonical (S-expression)

;; AFFINE-1A: Basic double-use → E6010
;; move param used twice in same scope
(arcana-ast :version 1 :module "test_affine_1a"
  (dc-mod
    :name "main"
    :items (
      (dc-fn :fn
        (fn-decl
          :body (block
            :stmts (
              (st-let :expr (ex-ident :name "h") :mut #f :pat (pat-ident :name "first_use"))
              (st-let :expr (ex-ident :name "h") :mut #f :pat (pat-ident :name "second_use")))
            :expr (ex-ident :name "first_use"))
          :contracts ()
          :effects ()
          :name "double_use"
          :params (
            (param :modifier move :name "h" :type (ty-named :path "Int")))
          :ret (ty-named :path "Int")
          :tparams ()
          :vis pub)))))

Human view

pub fn double_use(move h: Int) -> Int {
  let first_use = h
  let second_use = h   // → E6010 [AFFINE-USE-AFTER-MOVE]: 'h' used after move
  first_use
}

The move modifier on parameter h is the affine declaration — h may be consumed exactly once. The second let second_use = h is the violation; the compiler refuses the program. The canonical form spells out every AST node; the human view above is the projection that arcana view will render once the bidirectional CLI ships at v1.7.8 (D-489 council ratification).

The affine discipline catches a class of bugs that no amount of testing reliably catches in mainstream languages: forgotten close, double-close, leaked connection on an error path. The compiler refuses to emit the program.

Refinement types (scoped)

Refinement types narrow a base type with a predicate that must hold at every use site. A Username = String where len ≤ 32 is a String that cannot hold a 40-character value — the compiler enforces the predicate everywhere a Username is consumed, scoped to the predicate forms currently supported by the implementation (general-predicate refinement remains roadmap, not uniformly shipped). This catches a class of input-validation bugs at the type level rather than at runtime.

The current predicate subset is documented in the language specification (which publishes publicly alongside the v1.x complete release).

Compile-time data-flow / taint analysis (scoped)

Interprocedural taint analysis tracks how untrusted input flows through the program toward sinks — SQL queries, HTML templates, system calls. Common AI-generated injection patterns (direct interpolation of user input into a SQL string, unsanitised rendering into HTML) are caught at compile time within the coverage map documented in the spec — sophisticated variants (encoding-encoded injection, ORM-bypass, JSX-style attribute injection, and the rest of the named gap list below) still require explicit @sanitizer annotations or runtime sanitization at the boundary. (Throughout this page, WP-# refers to a numbered Work Package in the Arcana language specification; D# to a numbered design decision in the project’s public decision record.)

Below is render_valid_sanitized from tests/c30/fixtures/c30_valid_sanitized_html_rg7.arcana — a verified positive-case fixture showing the approved sanitization path. The sanitized_html() call is an allowlisted sanitizer that produces a SanitizedHtml value; the type system tracks the sanitization provenance, so the subsequent embed(content: safe, ...) call accepts it without a taint violation.

Canonical (S-expression)

;; C30 RG-7 fixture: valid sanitized_html() → embed(content:) — MUST compile clean.
;; SanitizedHtml via allowlisted sanitizer is valid input to embed.
(dc-fn :fn
  (fn-decl
    :body (block
      :stmts (
        (st-let :mut #f :pat (pat-ident :name "safe")
          :expr (ex-call
            :args ((arg-positional :expr (ex-lit :value (lit-string :value "<b>ok</b>"))))
            :fn (ex-ident :name "sanitized_html")))
        (st-expr :expr (ex-call
          :args (
            (arg-named :name "content" :expr (ex-ident :name "safe"))
            (arg-named :name "label" :expr (ex-lit :value (lit-string :value "X"))))
          :fn (ex-ident :name "embed"))))
      :expr (ex-lit :value (lit-int :value "0")))
    :contracts ()
    :effects (Render)
    :name "render_valid_sanitized"
    :params ()
    :ret (ty-named :path "Int")
    :tparams ()
    :vis pub))

Human view

pub fn render_valid_sanitized() -> {Render} Int {
  let safe = sanitized_html("<b>ok</b>")
  embed(content: safe, label: "X")
  0
}

The complement of this fixture — the negative case where raw unsanitised input flows into a render sink — emits E1221 (and the related XSS-marker codes named in WP-34 §7.1). The taint analysis tracks provenance across calls: a value that passed through sanitized_html() carries the SanitizedHtml refinement; raw String does not. The render sink’s contract accepts only SanitizedHtml, so the type system enforces the discipline at compile time without runtime checks.

This coverage is explicitly scoped, not comprehensive — the gap list is named below.

This coverage is explicitly scoped, not comprehensive. The gap list is named in the specification rather than hidden:

• Struct-field aliasing (s.field = user_input)
• Container / array-element aliasing
• mut re-assignment + dataflow on mutation
• Closure capture across non-resolvable indirect calls (currently conservative FULL_TAINT)
• Higher-order-function taint propagation
• HTML-entity encoding variants, case variants (<ScRiPt>), JSX-style attribute interpolation, event-handler attribute injection
• SQL concat-build patterns without typed-binding, ORM-bypass patterns

Sophisticated variants still require explicit @sanitizer annotations on the code path, or runtime sanitization at the boundary. The compile-time check catches what’s reproducibly catchable; the remainder is named explicitly so it’s not assumed.

Schema-as-types

One schema declaration becomes types + SQL + validation. A schema User { name: Username, email: Email, ... } declaration generates the Arcana type, the SQL CREATE TABLE, and the input-validation code — any drift between them is a compile error rather than a runtime mystery, because there is no drift surface: one declaration, three derivatives.

”If it compiles, it’s safe” — what it means here

This phrase is Arcana’s design aspiration, and it scopes precisely. It means: compile-time enforcement of declared effects, affine resource tracking, schema-as-type checks, and the common-pattern subset of taint analysis named above (per WP-34 §7.1). It does not mean coverage the implementation has not yet uniformly provided. The aspiration is not a blanket guarantee; the Honest Scope section names what’s covered and what isn’t.

On the roadmap (not yet implemented)

• Effect intersection / policy (D219) — the general [[effect_policy]] mechanism for SDK-declared intersection rules. Approved for a later release; not yet shipped.
• Full interprocedural dataflow beyond the named gaps above — per-gap roadmap in WP-34 §7.1.
• Refinement-type general predicates — broader predicate forms beyond the currently-shipped constructor subset.

These are intent, not commitment. See the Planned ≠ committed note in Honest Scope.

What this pillar gives every other pillar

• Effect Contracts & Capability Discipline rests on the effect system above — the contracts that travel from authoring through checking to deployment are typed using this layer.
• Batteries-Included is safer because the first-class effect capabilities {Email}/{SMS}/{CRM}/{Network}/{ObjectStore}/{Monitor} are enforced through the effect system, not bolted onto an untyped surface.
• Governance & Honest Scope is honest because this layer carries the actually-shipped guarantees — the marketing-claims ledger’s approved claims pin to mechanisms named on this page; the rejected claims are the over-aggregating shapes this layer cannot honestly support.

See Honest Scope for the canonical disclosure of what’s bounded, what’s gapped, and where the boundaries currently are.