Ownership you never have to annotate.

Why it exists

Three refusals, each with the thing it is refusing for. None of them is free, and the prices are in the rationale rather than hidden.

The claim, and the program that carries it

Two borrows go into denser and one comes back out. Which one it is depends on the values, so the compiler has to prove the returned borrow outlives the call. In Rust that proof is spelled <'a> three times in the signature. Here it is nowhere, and the guarantee is the same.

type Sample:
    kelvin: F64
    grams: F64

# Two borrows go in and one comes back. Which one depends on the values, so
# the compiler has to prove the answer outlives the call. That proof is the
# whole of what a lifetime annotation would have told it.
def denser(a: borrowed Sample, b: borrowed Sample) -> borrowed Sample:
    if a.grams >= b.grams:
        a
    else:
        b

let core be Sample(kelvin: 5778.0, grams: 12.5)
let shell be Sample(kelvin: 4100.0, grams: 3.25)

# `denser` declares its parameters `borrowed`, so the call site is bare.
let winner be denser(core, shell)
print(f"{winner.kelvin} K at {winner.grams} g")   # => 5778.0 K at 12.5 g

Checked and built with sciencec check density.science and sciencec build density.science; the trailing comment is what the linked binary printed. The call site is denser(core, shell) and not denser(&core, &shell) because a parameter declared borrowed is borrowed automatically — Rust rejected that, Mojo adopted it, and for this audience Mojo is right.

The checking is real, which is the only way the claim means anything

Inference without enforcement is a language that compiles everything. Overlap a shared borrow with an exclusive one and the same compiler that asked for no annotations refuses the program, points at all three lines that make the conflict, and names the two fixes.

error[SC0330]: `core` is borrowed here and borrowed exclusively before the borrow ends
  --> overlap.science:10:1
   |
 9 | let view be borrowed core
   |             ------------- `core` is borrowed here, shared
10 | warm(core)
   | ^^^^^^^^^^ ...and borrowed here, exclusively
11 | print(f"{view.kelvin}")
   |       ---------------- the first borrow is still needed here
   |
   = note: a shared borrow and an exclusive one cannot overlap (§6.1 rule 4)
   = note: the borrow ends at its last use, so moving the last use above the conflicting line is enough; binding what is needed before it is the other fix

Verbatim from sciencec check overlap.science, which exits 1. examples/21_compiler_shapes.science is the harder version of this test: a flat index-keyed table with parent links, a type holding a borrowed array in a field, a boxed recursive tree and a work-queue traversal, all taken from the Rust compiler in crates/ rather than invented, and it passes the borrow checker with no region written anywhere.

The rest of it reads the way the audience already writes

choice Phase:
    Solid
    Liquid
    Gas

type Reading:
    kelvin: F64
    pascals: F64

def phase_of(r: borrowed Reading) -> Phase:
    if r.kelvin < 273.15:
        Solid
    else:
        if r.kelvin < 373.15:
            Liquid
        else:
            Gas

def report(r: borrowed Reading):
    match phase_of(r):
        Solid: print(f"{r.kelvin} K: solid")
        Liquid: print(f"{r.kelvin} K: liquid")
        Gas: print(f"{r.kelvin} K: gas")

report(Reading(kelvin: 260.0, pascals: 101325.0))    # => 260.0 K: solid
report(Reading(kelvin: 400.0, pascals: 101325.0))    # => 400.0 K: gas

Built and run the same way. Equality is is and ordering is >=, with no second spelling of either, so a formatter has nothing to normalise and generated code cannot drift. The full surface is in the reference.

Measured against what you already use

Four comparisons, each making one point. The long form — including the ones where Science comes off worse — is in the rationale.

Rust — the same guarantee, none of the notation

denser above is fn denser<'a>(a: &'a Sample, b: &'a Sample) -> &'a Sample in Rust, and the call site is denser(&core, &shell). Science writes neither the parameter nor the ampersands, and still rejects the overlapping-borrow program above with a span on every line involved. The difference is not politeness: Rust's elision rules are a convenience over a syntax that stays available when the guess is wrong, and Science has no syntax to fall back on, so inference has to be total. That is the expensive half of the design, and it is why interprocedural analysis is mandatory here and optional there.

Python — the same mistake, one run earlier

Passing a string where a float belongs is a TypeError in Python at the moment the line executes, which on a training job is after the data has loaded. Here it is a compile error with a span, and the program never starts:

error[SC0525]: expected `F64`, found `String`
 --> ratio.science:5:15
  |
5 | print(f"{half(reading)}")
  |               ^^^^^^^ this is `String`

sciencec check ratio.science, exit 1. Python's own type hints would have described the same mistake and not stopped it, because nothing in CPython checks them.

Go — the error model, and not the memory model

Science took Go's answer to failure over the alternatives: a function that can fail returns its value beside an error, -> (T, Error?), and ? is a total presence test that produces a Bool and cannot return from the function around it. It did not take Go's answer to memory. The written-down run-time target is scalar code within roughly 20% of an equivalent Rust program, with Go expected behind both, and the reason given is structural rather than effort: no write barrier on pointer writes, monomorphisation instead of one copy per GC shape, and an optimiser that can vectorise. The same note prices the other side honestly — Go is the right target for compile time and the project expects to miss it badly, for the three reasons it lists. Both of those are targets. Nothing has been benchmarked, and no number on this page is a measurement of speed.

C — declared, linked, and nothing in between

There is no header parser, no generated shim crate and no wrapper layer. An extern block is a declaration in the language, and the program below links against libm and runs.

# libm is a C library nobody is going to rewrite. Declaring it is the whole
# of the binding: no header parse, no generated shim, no wrapper crate.
unsafe extern "C" library "m":
    def cos(x: F64) -> F64
    def sqrt(x: F64) -> F64

let c be unsafe: cos(0.0)
let r be unsafe: sqrt(2.0)
print(f"cos(0) = {c}, sqrt(2) = {r}")
# => cos(0) = 1.0, sqrt(2) = 1.4142135623730951

Built with sciencec build libm.science and run; the trailing comment is the binary's output. The backend itself is held to the same rule: it talks to LLVM through extern "C" against LLVM-C, and no crate in the workspace depends on inkwell, llvm-sys or cranelift — which is a commitment, not an accident, because a Science-hosted backend could not call a Rust wrapper.

Where the compiler actually is

sciencec is version 0.0.1 and there is no installer, no package and no released binary. What follows is split into what has been run and what has not, because a page that overstates is one a single question destroys.

Claims, and the command that settles each one

The test count is a snapshot and the command beside it is the point: it went from 1,884 to 1,913 during the afternoon this page was written, so take the number as evidence that the suite is run rather than as a constant.

The twenty-second is 17_modules.science, and it fails for a reason worth stating rather than hiding: it opens with use text.parser, and this repository contains no text module, so SC0202 is correct and the file is a fixture ahead of its fixtures. The corpus is input data for the test suites, so anything else there that failed would be a bug in the compiler rather than a typo to patch.

What is not built, in the compiler's own words

check is much further along than build. The program below passes the whole front half — it lexes, parses, resolves, type-checks and clears the borrow checker — and then the backend refuses it, because String.length has no MIR body to emit:

let name be "Ada"
print(f"{name.length()}")   # `check` exits 0; `build` refuses, below

error[SC0400]: this `sciencec` cannot build a call to `length`, which this crate was given no MIR body for
  = note: this `sciencec` implements §10's stages 0 to 3 of `codegen-and-linking.md` and some of what comes after — a script body, string literals and `print`, `extern "C"` declarations and the calls to them, the CFG, scalar arithmetic, functions with parameters, records, `choice`s and `match`, `T?`, and drops of values that own nothing — and refuses everything else rather than lowering a construct no execution test has ever run

Both lists were probed one program at a time against the tree on the day this page was written, not copied from a roadmap, and the boundary between them moves — tuples and casts crossed it while the page was being checked. The quoted note above is the compiler's own and is the version that ships with it; build on anything in the right-hand column prints its own reason, which is always more current than this paragraph.

The reason the refusals are this specific is a rule the backend is held to: every construct it admits is gated by a program that is built, linked, run and checked for its output. That rule was not free advice. Five silent miscompiles have been found by running the output rather than reading it — a main that never wrote its return value, an eight-byte store into a one-byte slot that passes LLVMVerifyModule, a needs_drop blind to every runtime aggregate, a lowering hole that suppressed the borrow checker over whole bodies, and a pointer-to-pointer the verifier structurally cannot catch. In this half of a compiler, silence does not mean it works.

The toolchain, as it exists

$ sciencec --version
sciencec 0.0.1
$ sciencec check density.science
$ echo $?
0
$ sciencec build density.science && ./density
5778.0 K at 12.5 g

check is silent on a clean file and exits 0, so it drops into a shell script or a CI job without ceremony. Diagnostics go to stderr and dumps go to stdout, which is what makes the dumps pipeable. Every diagnostic carries a code and a span, and where a mechanical fix exists it carries the replacement text too, so an editor or an agent can apply it without reading the prose.

check / build

Run the front half and report what is wrong; then, for build, produce an executable.

fmt

Print the file formatted to stdout, or rewrite it with --write. It refuses any file that does not already lex and parse, because reformatting a guessed token stream is how a formatter eats a program.

tokens / ast / resolve

Dump the token stream, the syntax tree or the resolved crate, for when you want to see what the compiler saw.

tools --json

A JSON Schema for every tool in the file, derived from the signature rather than written beside it.

Documentation

The specification is the authority. Forty-two design notes decide one area each, state what they rejected and why, and price what they ask of the others — including, in several places, a conclusion reached against the brief the note was given.

Programs that must fail live beside them in tests/ui/, each paired with the exact diagnostic it has to produce, rendered byte for byte. That is why the error blocks on this page are transcripts rather than illustrations.