Panic, Assertions and Runtime Checks

Panic and Recoverable Errors Are Different

Expected failures should remain ordinary typed program states:

fn Open(path: string) Result[File, IOError] {
    ...
}

Examples that normally belong in a recoverable channel include:

• invalid user input;
• file not found;
• disk full;
• connection failure;
• timeout;
• allocation failure where recovery is supported;
• missing optional data.

Panic is instead appropriate for conditions such as:

• failed internal assertions;
• reached checked unreachable;
• runtime safety checks whose ordinary form cannot prove safety and is not handled through try;
• other invariant failures whose owning language rule explicitly selects panic semantics.

Returning Err(errorValue) is normal completion through the recoverable result channel. It is not panic.

Runtime Safety Checks

Sec uses checked semantics for operations where invalid runtime input could otherwise violate the language's guarantees.

Runtime-check categories include:

• integer overflow where the operation is checked;
• division or remainder by zero;
• invalid shift counts;
• invalid narrowing or scalar conversion;
• array and slice bounds;
• invalid slice ranges;
• shape/dimension incompatibility;
• named-type contract failure;
• invalid reference generation or expired arena reference where runtime validation is required;
• invalid representation at a trusted boundary;
• assertion failure;
• reached checked unreachable.

Statically provable ownership violations remain compile-time errors rather than runtime checks.

Checked Operations Have Three Compiler Outcomes

1. Proven safe

When the compiler proves the failure condition impossible, no runtime failure path remains:

type Small int range 0..100

fn Increment(value: Small) int {
    return value + 1
}

2. Fallible

Using try converts the check into explicit typed fallible control flow:

let total := try left + right
let value := try values[index]

The owning operation defines the exact error type, such as ArithmeticError or IndexError.

3. Panic-capable

When the ordinary checked operation is used and failure cannot be disproven, the operation may panic:

let total := left + right
let value := values[index]

If the runtime failure occurs, panic semantics determine what happens to the current execution domain.

Checks May Be Eliminated by Proof

The compiler may prove runtime checks unnecessary through facts such as:

• constant evaluation;
• range and other named-type contracts;
• branch refinement;
• successful assert refinement;
• loop induction;
• fixed lengths or capacities;
• generic constant arguments;
• call-site specialization;
• whole-program analysis where available.

if index >= 0 && index < values.Length {
    let value := values[index]
}

Inside the true branch, the compiler may prove the bounds check redundant.

Removing a proven-unnecessary check does not change program semantics.

Core Panic Rule

When panic occurs:

• the current panic domain terminates;
• the failed stack never resumes;
• code after the panic point does not continue in that domain;
• panic remains visible to compiler effect analysis;
• panic does not change the declared function return type;
• panic is not implicitly converted into Err.

Another execution domain may later observe the panic outcome when the active concurrency model defines a containment boundary, but the failed operation itself did not return normally.

Panic Domains

A panic domain is the execution unit terminated by panic.

Canonical categories include:

• managed task;
• managed thread;
• root process domain;
• freestanding or bare-metal root domain.

An ordinary function call is not itself a panic domain. Panic is not implemented by secretly adding a hidden error result to every function.

No General Panic Catching

Sec 0.1 has no ordinary language construct equivalent to:

try {
    ...
} catch panic {
    ...
}

and no general:

• catch-and-resume;
• recover-and-continue;
• catch-all exception mechanism.

Panic may be observed only through a canonical containment boundary such as an awaiter, joiner, supervisor, test harness or root panic endpoint.

Observation of a terminated domain never resumes its failed stack.

Root Panic

Hosted programs

Panic in the root process domain terminates the process. No normal continuation follows.

A selected platform/profile may perform bounded panic-safe reporting, permitted cleanup, debugger trapping or a configured hook before final termination.

Freestanding and bare-metal programs

A root panic transfers control to the configured non-returning panic endpoint. Possible policies include:

halt
reset
enter safe state
write diagnostic register
signal watchdog
signal hardware
trap to monitor/debugger

Contained Panic in Managed Execution

A managed task or managed thread may form a containment domain. Panic terminates that domain while another domain observes a panic outcome according to the concurrency contract.

An ordinary contained task/thread panic does not automatically terminate the process.

Conceptually, a task outcome includes a distinct panic state:

type TaskOutcome[T] union {
    Completed(T)
    Cancelled
    Panicked(PanicInfo)
    Failed(TaskError)
}

Panicked(PanicInfo) remains distinct from normal Failed(TaskError) and from a function returning Err(E).

PanicInfo

Sec 0.1 defines a bounded portable panic-information value:

type PanicInfo struct {
    ID: PanicID
    File: string
    Line: uint
    Column: uint
    Function: string
}

These five fields form the portable Sec 0.1 surface.

A profile may provide richer diagnostic information such as a message, operation, task/thread/process identity or call stack, but that does not change this portable struct.

PanicInfo is bounded observation metadata. Copying it transfers no ownership of the failed execution domain.

PanicID

The stable panic-reason identifier is:

type PanicID uint32

It is target-independent and identifies a registered panic reason.

Canonical panic reason categories include at least:

• arithmetic overflow;
• division by zero;
• invalid shift;
• bounds failure;
• contract failure;
• assertion failure;
• checked unreachable reached;
• invalid reference generation;
• explicit panic;
• foreign abort or trusted-boundary failure.

The numeric registry and exact stable reason spelling belong to diagnostics/panic registry data rather than to source programs.

The Minimum Panic Path Is Allocation-Free

Panic reporting must have a minimum path that does not require:

• heap allocation;
• dynamic string concatenation;
• growing collections;
• symbolization;
• filesystem or network access;
• blocking on a potentially compromised allocator.

Static metadata or constant tables may provide source information without allocating at panic time.

A profile may add richer reporting only when it remains compatible with the active panic-context guarantees.

Assertions

assert checks programmer/internal invariants.

It is not intended for ordinary recoverable input or business validation.

Canonical Assertion Syntax

Sec 0.1 defines exactly these ordinary forms:

assert condition

assert condition, "message"

The comma is the canonical separator before the optional message.

Function-style assertion syntax is not canonical:

assert(condition)    // not the canonical Sec assertion form

The optional message is a string literal in Sec 0.1. Dynamically constructed assertion messages are not part of the current syntax.

Assertion Conditions Must Be bool

assert count > 0

assert state == State.Ready, "state must be ready"

Sec applies no truthiness conversion.

This is invalid when count is not already bool:

assert count

Assertion Semantics

If the condition is true, execution continues normally.

If the condition is false, the current panic domain panics with the stable assertion-failure reason.

The optional message adds static diagnostic information. It does not create a recoverable error value.

Assertion condition evaluation follows normal Sec expression evaluation and side-effect rules.

Successful Assertions Refine Analysis

assert index >= 0 && index < values.Length
let value := values[index]

After the successful assertion, the compiler may use the proven condition as a control-flow fact.

A later redundant bounds check may therefore be removed when proof is complete.

Assertions Are Always Semantically Active

Ordinary assertions have the same semantic meaning in debug and optimized builds.

Optimization level alone does not disable them.

The compiler may remove an assertion only when it proves the condition true for every path reaching it.

Sec 0.1 has no separate ordinary debug assert form.

Assertions Are Not Business Validation

Use assert for invariants such as:

assert state == State.Initialized
assert count <= capacity

Use recoverable error handling for expected invalid input:

fn SetPercentage(value: int) Result[void, ValidationError] {
    ...
}

assert is not an unchecked optimizer promise. Sec 0.1 exposes no ordinary safe-language assume.

Checked unreachable

Canonical syntax:

unreachable

Reaching the statement panics the current domain with the stable checked-unreachable reason.

If the compiler proves the statement unreachable, no panic path remains.

This is deliberately not backend undefined behavior. Backend unreachable may appear only after the path has been proven impossible or after a defined non-returning Sec panic/trap path.

Explicit Programmer-Triggered Panic

What is already locked regardless of future syntax:

• explicit panic terminates the current panic domain;
• it never returns to the failed stack;
• it contributes a panic effect;
• it is incompatible with unresolved @noPanic;
• its minimum representation must be allocation-free;
• it has a stable explicit-panic reason category.

This section must be rewritten when the grammar and payload contract are formally decided.

@noPanic

@noPanic is a compiler-verified transitive guarantee:

@noPanic
fn Calculate(...) Result[Money, CalculateError] {
    ...
}

It means that no reachable language-defined panic remains on any valid execution path covered by the contract.

A function returning Result may still be @noPanic; recoverable Err is not panic.

@noPanic Is Proven Transitively

Proof includes:

• direct panic-capable operations;
• direct and indirect calls;
• generic specializations;
• callbacks;
• FFI effect contracts;
• compiler-generated helpers;
• cleanup and defer;
• destruction;
• runtime checks.

Unknown required effect information is not positive proof of no-panic behavior.

An assertion inside @noPanic is valid only when the compiler proves its condition true at every reachable point:

type NonNegative int range 0..int.Max

@noPanic
fn Use(value: NonNegative) int {
    assert value >= 0
    return value
}

Likewise, checked unreachable is valid in a no-panic function only when it is proven unreachable.

ISR Interaction

Sec 0.1 interrupt-safe execution is no-panic.

Therefore ISR analysis rejects reachable:

• unproven assertions;
• reachable checked unreachable;
• panic-capable runtime checks;
• panic-capable calls;
• panic-capable cleanup;
• unknown foreign abort behavior;
• future explicit panic.

unsafe does not waive the no-panic requirement.

A proven-safe checked operation or proven assertion contributes no remaining panic effect.

Panic Cleanup

Cleanup behavior depends on the selected panic policy and the execution domain.

Where the panic policy guarantees cleanup, cleanup may include:

• reached defer entries;
• automatic destruction;
• task/thread-local cleanup;
• containment bookkeeping;
• panic-sink notification.

Cleanup that must run on panic is itself required to be transitively no-panic.

A target/profile selecting immediate trap, reset or no-cleanup root behavior does not guarantee pending ordinary root-domain cleanup.

Double Panic

A panic during required panic cleanup violates the no-panic cleanup contract.

If a second panic nevertheless occurs because of unsafe code, foreign code, hardware corruption, compiler defects or incorrect trusted metadata, the current panic domain terminates immediately through the minimal panic endpoint.

A second cleanup sequence is not started.

Contained Panic Does Not Guarantee Shared-State Consistency

Panic containment means an execution domain can terminate without necessarily killing the entire process.

It does not guarantee that partially modified shared state remains logically valid.

Programs that continue after contained panic may need strategies such as:

• transactional updates;
• copy-then-commit;
• message passing;
• task-owned state;
• version validation;
• rollback;
• poisoning.

Synchronization primitives may define poisoning, but poisoning is not mandatory for every primitive.

Panic, Result and Cancellation Stay Distinct

Err(errorValue)     // normal recoverable return
Panicked(PanicInfo) // abnormal terminated domain
Cancelled           // cancellation outcome

Panic is never automatically converted into Err.

Cancellation is not panic.

A supervisor may choose to cancel sibling work after observing panic, but that policy does not make the two concepts equivalent.

Unsafe and FFI Do Not Disable Panic Rules

unsafe does not waive @noPanic or panic-domain requirements.

Foreign exceptions or unwind must not cross Sec frames unless a future dedicated FFI rule explicitly defines and proves such behavior.

Unknown foreign behavior is not positive proof of @noPanic.

Trusted FFI or unsafe metadata may establish a proof boundary only where the canonical FFI/unsafe rules permit it.

Target Panic Strategy

A target/profile may select root behavior such as:

• cleanup then terminate;
• limited cleanup;
• immediate termination;
• trap;
• reset;
• custom endpoint.

Portable code must not depend on one root panic cleanup strategy unless its selected profile explicitly guarantees that strategy.

No target/profile may redefine panic as hidden recoverable exception flow.

No Mandatory General Runtime

Panic support does not require a general Sec runtime.

A panic endpoint may be implemented as:

• a compiler-emitted non-returning function;
• a user-provided function;
• a target support symbol;
• a scheduler hook when managed scheduling is used;
• a direct target trap;
• a test-harness boundary.

A freestanding program may implement panic behavior without allocator, scheduler, unwinder or general runtime library.

A program proven completely panic-free may eliminate unreachable panic support.

Compile-Time Evaluation

If a panic path or failed assertion is reached during required compile-time evaluation, the compiler reports compile-time evaluation failure with source provenance.

The compiler itself must not crash and does not materialize a runtime panic merely because the evaluated Sec expression would panic.

By contrast, a normal Result.Err(...) is an ordinary successfully evaluated Sec value.

Diagnostics

Panic diagnostics should explain:

• the panic-capable operation;
• the concrete reason;
• the relevant source/call path;
• the violated guarantee, such as @noPanic;
• the missing proof;
• a practical recoverable or provably-safe alternative when known.

Unchecked overflow risk in no-panic code

`CalculateInvoiceTotal` is not panic-free

call path:
    CalculateInvoiceTotal
    -> CalculateLine
    -> quantity * unitPrice

signed multiplication may overflow

help: use `try`
help: constrain the operands
help: widen explicitly
help: choose an explicit wrapping or saturating operation when that matches the domain

Unproven assertion

assertion may fail in `@noPanic` code

the compiler cannot prove:
    index < values.Length

help: establish the bound before this point
help: use a recoverable check when failure is an expected outcome

Reachable unreachable

`unreachable` may be reached

checked `unreachable` panics when execution reaches it

help: make the control-flow proof complete
help: handle the remaining state explicitly

The LSP and sec analyse should consume the same panic-effect facts and proof results as compilation.

Required Future Updates for This Page

This page is intentionally usable now, but it must be revisited before the Sec 0.1 manual is considered complete.

Best Practices

• Use typed recoverable errors for expected failures.
• Reserve panic for broken invariants and language-defined unrecoverable checked paths.
• Use try when a runtime check should become a recoverable typed failure.
• Use assert for invariants, not input validation.
• Do not rely on assertions disappearing in optimized builds.
• Use checked unreachable only when reaching the point represents a broken invariant.
• Use @noPanic when the API or execution context requires a verified panic-free call graph.
• Do not assume panic cleanup occurs unless the active execution-domain/profile policy guarantees it.
• Do not assume contained panic leaves shared mutable state logically consistent.
• Keep panic sinks and root endpoints bounded and allocation-free on their minimum path.
• Do not use illustrative explicit-panic syntax until that grammar is formally locked.

Summary

• Panic is for broken invariants and operations whose canonical ordinary failure semantics select panic.
• Expected recoverable failures use Result, Option, typed errors, try, match and ordinary control flow.
• A runtime-checked operation may be proven safe, made fallible with try, or remain panic-capable.
• The compiler may remove runtime checks only when the relevant failure is proven impossible.
• Panic terminates the current panic domain and never resumes the failed stack.
• An ordinary function call is not itself a panic domain.
• Sec 0.1 has no general user-level catch-and-resume panic mechanism.
• Managed task/thread panic may be observed at a containment boundary without automatically terminating the entire process.
• Contained Panicked, returned Err and Cancelled remain distinct outcomes.
• Hosted root panic terminates the process.
• Freestanding root panic transfers to a configured non-returning endpoint.
• The exact project/profile configuration syntax for root panic policy must be documented later.
• PanicID is type PanicID uint32.
• PanicInfo contains ID, File, Line, Column and Function.
• The minimum panic path is allocation-free.
• Canonical assertion syntax is assert condition or assert condition, "message".
• Assertion conditions must be bool; Sec has no truthiness conversion.
• A failed assertion panics the current domain.
• Assertion messages are static string literals in Sec 0.1.
• Assertions remain semantically active in optimized builds.
• An assertion may be removed only after proof that it always succeeds.
• A successful assertion may refine later compiler analysis.
• Assertions are for invariants, not expected business/input validation.
• Sec 0.1 has no ordinary debug-only assertion form and no ordinary safe-language assume.
• unreachable is checked and panics when reached.
• Checked unreachable is not optimizer undefined behavior.
• The exact explicit programmer-triggered panic syntax and payload are not yet locked and this manual section must be rewritten later.
• @noPanic is a transitive compiler-verified guarantee.
• No-panic proof includes calls, generics, callbacks, FFI contracts, cleanup, destruction and runtime checks.
• An unproven assertion contributes a panic effect.
• A proven assertion contributes no remaining panic effect.
• ISR/interrupt-safe execution in Sec 0.1 requires no-panic behavior.
• Unsafe does not waive no-panic or ISR panic restrictions.
• Panic cleanup runs only where the active panic policy guarantees it.
• Required panic cleanup must itself be panic-free.
• A second panic during panic cleanup terminates immediately through the minimal endpoint without starting another cleanup pass.
• Containment does not guarantee consistency of partially modified shared mutable state.
• Target/profile panic strategy may choose cleanup, limited cleanup, immediate termination, trap, reset or another defined endpoint.
• No profile may redefine panic as hidden recoverable exception flow.
• Panic support requires no mandatory general Sec runtime.
• A fully panic-free program may eliminate unused panic support.
• Compile-time evaluation reports reached panic/assert failure as compile-time evaluation failure rather than crashing the compiler.
• The exact explicit panic syntax, profile configuration, concurrency observation APIs and final cleanup integration remain marked for manual update.