1. Ownership, moves, and checked borrows

An owning value has one cleanup responsibility. Moving it transfers that responsibility and makes the old place unavailable until it is reinitialized. Copying is reserved for values whose semantics permit independent copies.

A checked &T or &const T borrow does not take ownership. Its lifetime keeps the owner alive and prevents conflicting access. A checked slice adds a length to that borrowed access, so indexing remains bounds-checked. Keep borrows short, return owned data when a caller must outlive the source, and let compiler diagnostics expose ambiguous ownership instead of reaching for raw pointers.

Study checked references, checked slices, and the memory model. Then modify an owned collection while a view is live and read the rejection as a statement about resource identity.

Tested example

Follow one value through mutable reborrowing, a moved handle, and shared read-only handles.

File: curriculum/main-evidence/single/checked_references.fl

// Build: build/flecha build examples/checked_references.fl -o build/checked_references
// Prints 6 and exits with 6.

void double_value(&u8 value) {
    *value = *value * 2;
}

u8 read_value(&const u8 value) {
    return *value;
}

i32 main() {
    u8 value = 3;
    ref := &value;
    double_value(ref); // A call reborrows; ref remains usable.
    stdoutln(read_value(ref));

    // The last use of ref has passed, so value is accessible directly.
    u8 other = 10;
    moving := &other;
    moved := moving; // moving cannot be read until reassigned.
    *moved = 11;
    moving = &other;
    *moving = 12;

    constref u8 fixed = &other; // const &u8: fixed binding, writable target.
    *fixed = 13;
    &const u8 shared = &other;
    copy := shared; // Shared handles may be copied.
    if *copy != *shared { return 1; }

    *u8 pointer = none;
    slot := &pointer; // &*u8: a checked reference to a raw-pointer variable.
    *slot = none; // Safe access to the pointer slot; no pointee access.

    return value as i32;
}

The block above is the complete file executed by the commands below.

Each binding represents a distinct ownership or borrowing operation. Reading the sequence in order shows when mutation is allowed, when a handle moves, and when only shared reads remain valid.

Commands

flecha check curriculum/main-evidence/single/checked_references.fl
flecha build curriculum/main-evidence/single/checked_references.fl -o build/checked_references
build/checked_references

Expected output

6
exit status: 6

Related reference: /examples/checked_references/.

1. Ownership, moves, and checked borrows

Tested example

Commands

Expected output

What to learn next