Formal Safety Model #

SafeC's safety guarantees are not aspirational — they are formalized as a type system with syntactic type safety (progress + preservation), drawing on prior work from Oxide (Weiss et al.) and Cyclone (Grossman et al.).

Seven Safety Properties #

1. Spatial Safety #

No out-of-bounds memory access. Array subscripts are bounds-checked at compile time for constant indices and at runtime for dynamic indices.

int arr[4];
arr[5] = 1;        // compile-time error: index 5 out of bounds for array of size 4

int i = get_index();
arr[i] = 1;        // runtime bounds check inserted (abort on violation)

Runtime bounds checks can be suppressed inside unsafe {} blocks.

2. Temporal Safety #

No use-after-free: region annotations tie reference lifetimes to allocation scopes. A reference to stack memory cannot escape the function, a reference into an arena is invalidated by arena_reset<R>()/arena_destroy<R>()/arena_free_to<R>(), and a &heap T reference is invalidated by std::dealloc() — all three are checked at compile time, not just at runtime.

&stack int get_local() {
    int x = 42;
    return &x;      // compile-time error: stack reference escapes function
}

#include <std/mem.h>

void heap_example() {
    &heap int p = new int;
    std::dealloc(p);
    *p = 1;              // compile-time error: use of 'p' (&heap reference) after std::dealloc() freed it
    std::dealloc(p);      // compile-time error: double-free, same check
}

3. Aliasing Safety #

Mutable references are exclusive. The borrow checker enforces that at any point in the program, a value has either one mutable reference or any number of immutable references, but never both simultaneously.

int x = 10;
&stack int a = &x;          // mutable borrow
&stack const int b = &x;    // error: cannot borrow 'x' as immutable: already borrowed as mutable

const &stack int b is the same type as &stack const int b: const may go on either side of the region qualifier.

4. Region Escape Safety #

References cannot outlive the region they point into. The compiler tracks region scope depth and rejects any assignment or return that would move a reference to a shallower scope.

region R { capacity: 1024 }
&arena<R> int outer_ptr;

void demo() {
    &arena<R> int p = new<R> int;
    outer_ptr = p;   // error: cannot assign '&arena<R> int' to variable in
                     //        outer scope: arena reference would escape
}

5. Data Race Freedom #

Every type is Send and/or Sync, derived from its structure (overridable with unsafe impl Send; / impl !Send;). spawn accepts only static data a thread may share, spawn_scoped lends a local until it is joined, thread_spawn and channels move Send values, and Mutex<T> reaches its value only through a guard — so safe code can't share mutable state across threads without synchronization. See Thread Safety.

6. Null Safety #

References are non-null by default. There is no null reference in safe SafeC code. Nullable references use the ?&T syntax; unlike languages with flow-sensitive null narrowing, a bare != null comparison does not by itself make a later dereference safe — reading a nullable reference is only sanctioned through match, .is_null(), .default(fallback), or an explicit unsafe block (see Safety).

7. Determinism #

No hidden runtime costs. SafeC does not insert garbage collection, reference counting, or implicit heap allocations. Every allocation is explicit in the source code. The performance model is transparent — what you write is what runs.

Memory Safety Compared to C, C++, Rust, and Zig #

Comparison has a one-line "Memory Safety: Yes/No" summary across the same five languages; this breaks that single row out into the properties above, since "yes" and "no" hide real differences in when each language checks (compile time vs. runtime vs. not at all) and how completely (every safe-mode program vs. an opt-in build mode vs. nothing).

The throughline: C and C++ don't check most of these at all (undefined behavior is the "checked" state most of the time). Zig checks several of them, but as a build-mode choice — the same source either has the checks or doesn't, decided once for the whole binary, not per-line. Rust and SafeC both check at compile time by default and require an explicit, lexically-scoped opt-out (unsafe {}) to turn a check off for a specific block of code — that's the property this page's own unsafe escape hatch section is describing. Where Rust and SafeC differ is how they prove temporal safety (ownership/borrowing vs. region membership — see Compared to Rust for that trade-off in detail) and how complete the proof is: Rust's borrow checker is a sound, complete static proof for the patterns it accepts (it may reject valid programs, but never accepts an unsound one); SafeC's region and lifetime checks are sound within stated trust boundaries (calls through function pointers and to bodiless extern functions, memory reached through raw pointers in unsafe {}) and may still reject a few valid shapes (a free and a use guarded by complementary conditions, a loop that frees a linked structure node by node — see Temporal Safety), trading some precision for a simpler, more C-compatible mental model.

Safety Analysis Phases #

The compiler enforces these properties through a series of analysis passes during semantic analysis:

All checks run at compile time. The only runtime insertion is bounds and range checks for dynamic array and slice indices, and those are visible in the generated IR.

The unsafe Escape Hatch #

All safety checks can be locally suppressed inside unsafe {} blocks:

unsafe {
    int* raw = (int*)some_addr;
    *raw = 42;       // no bounds check, no borrow check, no region check
}

unsafe is lexically scoped. It does not propagate to called functions. It serves as a grep-able marker for code that requires manual auditing.

FFI Boundary Rules #

Foreign function calls (C interop) follow specific safety rules:

• extern declarations use raw C types — no region qualifiers
• &static T to T* coercion is safe without unsafe {}
• &T/?&T (no region qualifier at all — an "outliving reference," see Memory & Regions) also coerces to/from T*/void* safely without unsafe {}, in both directions — the type for a pointer that may be retained by the C side past the call returning
• Non-static, non-region-less references passed to C require unsafe {}
• Raw pointers received from C must be handled inside unsafe {}, unless received directly into a &T/?&T-typed variable

These rules ensure that the boundary between safe SafeC code and unsafe C code is always explicit.

Formal Foundations #

The safety model is grounded in established type theory:

• Oxide (Weiss et al., 2019) — formalization of Rust's ownership and borrowing as a typed calculus with places and provenance
• Cyclone (Grossman et al., 2002) — region-based memory management with static safety guarantees for a C-like language

SafeC adapts these formalisms to a C-compatible language with regions as the primary memory safety mechanism.

Progress and Preservation #

The type system satisfies the standard syntactic safety properties:

• Progress: A well-typed program either is a value, can take a step, or is a sanctioned runtime error (bounds check failure with abort)
• Preservation: If a well-typed program takes a step, the resulting program is also well-typed

Together, these properties guarantee that well-typed SafeC programs do not exhibit undefined behavior outside of unsafe {} blocks.