Introduction

What Sec Is

Sec is designed for predictable native programs without requiring garbage collection, hidden reference counting, implicit exceptions, or a mandatory general-purpose runtime.

It combines high-level language features with low-level control. A program may use nominal types, contracts, units, generics, tagged unions, interfaces, properties, collections and structured error handling while still targeting operating systems, embedded systems, microcontrollers and bare-metal hardware.

Sec is influenced by many language traditions, including C, C++, C#, F#, Go, Rust, Zig, Ada, Vale and Odin. Those languages are sources of experience, not normative definitions for Sec. Familiar syntax may therefore have different semantics when Sec's own consistency or safety model requires it.

Intent and Proof

Sec tries to make syntax explicit when the programmer is making a real semantic choice, and implicit when the compiler can safely derive the bookkeeping.

Source code is expected to make choices such as these visible:

• mutability;
• fallible operations;
• unsafe operations;
• borrowing mode;
• ownership transfer from reusable values at consuming boundaries;
• external storage and hardware semantics;
• units and contracts that carry domain meaning.

By contrast, Sec avoids requiring annotations whose only purpose is to repeat information the compiler already knows or can prove.

The same principle applies to safety checks. Sec prefers to prove a condition at compile time. When proof is impossible but the language guarantee can be checked at runtime, the compiler may emit a check. When neither proof nor checking can provide the required guarantee, the program is rejected.

prove when possible
check when necessary
reject when neither can provide the required guarantee

Type System

Type identity in Sec is semantic, not merely representational. Two values may use the same machine representation and still be different types.

type CustomerID uint64
type ProductID uint64

let customer: CustomerID := 42
let product: ProductID := customer    // invalid

Named types are nominal. The compiler does not implicitly convert a typed runtime value merely because another type has a compatible underlying representation.

Contracts belong to types

Contracts describe valid values of a named type rather than ad-hoc restrictions on individual variables.

type Percent int range 0..100

let complete: Percent := 100
let invalid: Percent := 101            // compile-time error

Untyped literals may take their type from context. Converting an already typed runtime value is a different operation and is explicit.

let raw: int := ReadPercentage()
let value := try Percent(raw)

A checked conversion that the compiler can prove valid does not need a runtime check. The language semantics remain checked either way.

Units are semantic identity

Units are independent of their numeric carrier. The same unit may be represented by an exact decimal, a floating-point value or an integer where the declaration permits it.

let exactDistance: decimal<m> := 10
let measuredDistance: float64<m> := 10
let counterDistance: int64<m> := 10

Unit algebra is checked semantically. Numeric representation does not define unit meaning, and unit compatibility does not erase named-type identity.

Parameterized types

Generic arguments and compile-time shape information participate in type identity.

list[int]
Result[Data, IOError]

int[4]
byte[256]

vector[float64, 3]
matrix[float32, 4, 4]

Fixed arrays and dynamic owning sequences use postfix sequence syntax: T[N] and T[]. Borrowed sequence views use ref T[] or ref mut T[].

Error Handling

Errors are explicit typed values. Sec does not use hidden exception propagation as its ordinary error model.

The compiler-known lowercase type error is the common root of Sec error types. It is specific to the error system; it is not a general object base class and does not introduce ordinary inheritance.

enum IOError error {
    OpenError
    ReadError
    WriteError
}

A precise operation should normally expose its concrete error type:

fn Read() Result[Data, IOError]

An API that intentionally forwards heterogeneous Sec errors may instead use the open error channel:

fn RunPipeline() Result[Data, error]

Result[T, E] is must-use. Failure cannot silently disappear. try unwraps successful values and either handles or propagates the failure according to the surrounding context.

fn Load() Result[Config, IOError] {
    let data := try Read()
    let config := try Parse(data) {
        Err(error) => return Err(error)
    }

    return Ok(config)
}

match is the general exhaustive pattern-matching construct. try is the concise path when successful execution should continue normally and only failure needs special handling.

Memory Model

Sec uses deterministic ownership and compile-time analysis as the foundation for memory and resource safety. The language separates several concepts that are often conflated in lower-level programming:

• a value;
• a materialized object;
• a binding;
• a Place that identifies a usable program location;
• storage and storage lifetime;
• ownership responsibility;
• borrowing authority;
• reference validity and provenance;
• destruction and storage reclamation.

Ownership is semantic responsibility, not possession of an address. Moving a value transfers ownership; it does not inherently mean that bytes are relocated. Borrowing grants temporary authority without transferring ownership.

fn Inspect(value: ref Buffer) void {
    // shared access
}

fn Modify(value: ref mut Buffer) void {
    // exclusive mutable access
}

Safe references do not own their target. ref T provides shared access and ref mut T provides exclusive mutable access. Ordinary Sec source does not expose lifetime parameters.

Allocation, initialization, destruction and storage reclamation are separate operations. In particular, allocation provides storage; it does not by itself create a valid object. Destruction ends lifecycle responsibility; reclamation concerns storage.

Abstraction Without Losing Control

Sec does not treat high-level abstraction and low-level programming as opposites. A source-level abstraction is useful when it removes repetitive error-prone work while preserving semantically important behavior.

Behavior lives in impl

Stored representation belongs to the type declaration. Behavior and associated definitions belong to impl.

type Counter struct {
    value: int,
}

impl Counter {
    fn Increment() void {
        self.value += 1
    }

    fn Value() int {
        return self.value
    }
}

Instance methods receive compiler-provided implicit self. Canonical Sec methods do not declare ref self or ref mut self in their parameter lists.

A type has one primary implementation entry point. Additional same-module behavior may be organized in impl extends Type fragments. All fragments form one combined member surface.

impl extends Counter {
    fn IsZero() bool {
        return self.value == 0
    }
}

Explicit lifecycle construction

new selects lifecycle construction through init. It does not mean heap allocation.

impl Connection {
    init(address: Address) ConnectError {
        // establish a valid Connection
    }
}

let connection := try new Connection(address)

Conversion and lifecycle construction are separate operations: Type(value) is conversion; new Type(args...) is construction.

One Language Across Targets

Sec is intended for both hosted and freestanding environments. Core language semantics remain the same across desktop and server operating systems, embedded operating systems, microcontrollers and bare-metal targets.

A target profile may legitimately lack facilities such as heap allocation, threads, operating-system services, a particular ABI feature or runtime support. That may restrict which programs or libraries are available, but it must not silently redefine the meaning of the language.

The language avoids requiring a runtime whenever practical. Runtime validation does not automatically imply a general-purpose runtime; a check may lower directly to ordinary machine instructions or target-specific support.

Compiler Responsibility

Sec intentionally places substantial responsibility in the compiler. The programmer should not have to reproduce compiler-internal reasoning in source code.

The compiler model includes analyses such as:

• type and contract analysis;
• ownership, copy and move analysis;
• borrowing, lifetime and reference validation;
• escape and closure analysis;
• effect and control-flow analysis;
• definite assignment;
• destruction and cleanup planning;
• stack and recursion analysis;
• concurrency, data-race and deadlock analysis;
• ISR and platform validation;
• compile-time evaluation;
• unit analysis;
• ABI and FFI validation;
• optimization-legality analysis.

Diagnostics are part of that model. A compiler error should explain not only that a program is invalid, but which rule was violated, where the relevant values or declarations came from, why the conflict exists and, when useful, how it can be resolved.

Semantic analysis establishes Sec semantics. Later compiler stages preserve and lower those facts; the backend does not invent ownership, unit, lifetime, allocation or safety meaning from machine representation.

Example Program

This small example combines nominal typing, contracts, a struct, implicit self, typed errors and checked conversion.

module demo

import "fmt"

type Percent int range 0..100

enum InputError error {
    InvalidCompletion
}

type User struct {
    Name: string,
    Completion: Percent,
}

impl User {
    fn IsComplete() bool {
        return self.Completion == Percent(100)
    }
}

fn MakeUser(name: string, rawCompletion: int) Result[User, InputError] {
    let completion := try Percent(rawCompletion) {
        Err(_) => return Err(InputError.InvalidCompletion)
    }

    return Ok(User {
        Name: name,
        Completion: completion,
    })
}

fn main() Result[void, error] {
    let user := try MakeUser("Anna", 90)

    if user.IsComplete() {
        fmt.Println($"{user.Name}: complete")
    } else {
        fmt.Println($"{user.Name}: {user.Completion}")
    }

    return Ok()
}

Percent is a distinct named type whose contract belongs to the type. The runtime integer is converted explicitly because the conversion may fail. MakeUser exposes a precise error channel, while main deliberately accepts the open error channel and can propagate the concrete error without erasing its identity.

Language Status

Sec is currently being specified and implemented as version 0.1. The language manual describes the intended programmer-facing semantics. The normative rulebooks define the detailed language and compiler contracts, while implementation progress is tracked separately.

This separation matters. A feature may be fully specified before every compiler stage or target backend has implemented it.

Use the Implementation Status page when you need to know what the current compiler can execute end-to-end.

Non-Goals

Sec deliberately avoids several common language directions:

• no general class inheritance hierarchy;
• no ordinary hidden exception mechanism;
• no mandatory garbage collector;
• no hidden reference counting requirement;
• no automatic heap promotion merely to repair escaping values;
• no implicit expensive copying or resource acquisition;
• no assumption that new means heap allocation;
• no null safe references;
• no programmer-written lifetime parameters in ordinary source code;
• no globally implicit interface conformance;
• no backend-dependent reinterpretation of source-language safety rules.

The goal is not minimal language power. The goal is a language whose important semantics remain visible, predictable and explainable.