Science

Getting started#

A file is a module, and a file's top-level statements are its program. There is no project file, no manifest and no scaffolding — not even a main. Save this as hello.science.

type Reading:
    channel: Int
    counts: Int

def total(first: Reading, second: Reading) -> Int:
    first.counts + second.counts

let a be Reading(channel: 1, counts: 4_900)
let b be Reading(channel: 2, counts: 1_180)

print(f"channels {a.channel} and {b.channel} hold {total(a, b)} counts")
# channels 1 and 2 hold 6080 counts

$ sciencec check hello.science
$ echo $?
0
$ sciencec build hello.science
$ ./hello
channels 1 and 2 hold 6080 counts

Six things in eleven lines are worth naming before anything else, because each is a place a Python reader's expectations will quietly disagree with the language.

The statements at the top level are the program. There is no def main here and there must not be one: a file whose top level holds statements is a script, the compiler writes the main that runs them, and writing a second one yourself is SC0117. Scripts and programs is the section; the rule exists so that a two-line analysis script and a library module are the same file kind with no ceremony between them.

Blocks are indentation, and only spaces. A tab in the indentation is SC0003 with no attempt to guess a width. That is stricter than Python, which resolves the mixture by a rule most people could not state, and it is strict for a stated reason: a tab's width depends on how the file is displayed, so a file indented with both would mean different things to two readers of the same bytes.

let … be, not =. The word is there because = has two unrelated meanings in the languages this audience writes — binding in a program, equality in a paper — and a language that keeps the symbol for binding has to spell equality == to get out of the way. Science keeps the mathematical reading: is compares, be binds, and neither has a second spelling.

Reading(channel: …, counts: …) constructs with named arguments, in any order. Ordinary function calls are positional; record construction is not, and the asymmetry is deliberate. A record's fields have names the author chose, and a constructor call that lists four integers in an order you have to look up is one of the commonest places a program is silently wrong.

f"…" interpolates and "…" does not. A brace in a plain string literal is a brace, which is what makes JSON and LaTeX writable without escaping; the f prefix is what turns {total(a, b)} into a value. Any expression may stand in a hole. Strings and formatting has the rest.

check is silent on a clean file and exits 0. It drops into a shell script or a CI job without ceremony. Anything it finds goes to stderr with a code, a primary span and, where a mechanical fix exists, the exact replacement text, so an editor or an agent can apply it without reading the prose. Dumps go to stdout. Warnings alone do not fail the run.

What works today#

Documentation for an unfinished language is more useful when it says exactly where the edge is. This is where it is, area by area, as of this build — both halves, because a reference that overstates is one a single experiment destroys.

The front end: what check runs

sciencec check is seven phases, in this order, with a gate after each of the first three that stops the run when something was reported as an error: lex → parse → resolve → type-check (aliases, declarations, then bidirectional checking into THIR) → MIR lowering → the call graph → region inference. The gates are why a file with a syntax error never reports a borrow error: the later phase would be reasoning about a recovery rather than about the program.

The back end: what build emits, and what it refuses

The discipline is that nothing is lowered until an execution test has run it. Everything else is refused with SC0400 and a sentence naming the construct. That is a deliberately unusual choice — most compilers lower optimistically and find out later — and the reason is in this back end's own record: of the thirteen things reading the specification could not have established, three were silent miscompiles that verified, linked and ran. A main that never wrote its return value. A null test that loaded a fat pointer. A store eight bytes wide into a one-byte slot. None of those is a crash; every one of them is a number.

Two refusals in that list are worth reading twice, because they are smaller than they look and they bite in ordinary code. The first is for: the counting loop is the most-written construct in the language and no program containing one can be built today. The second is n be n + 1 — an assignment whose right-hand side reads a local — which check accepts and the back end refuses, because the value arrives untyped. let m be n + 1 builds; the assignment does not. Neither is a design decision; both are gaps, and they are named here rather than left for a reader to find with a program that ought to work. changing

error[SC0400]: this `sciencec` cannot build a value the front end left untyped: its `Ty` is `TyKind::Error` and no diagnostic was reported for it. The three this compiler has met are a call to `print` or `write`, whose signatures `science-resolve`'s `builtins.rs` withdrew; a `for` loop's range and iterator temporaries; and a discriminant temporary, which is handled rather than refused
  = 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

The backend is a build feature, and without it build is one message. cargo build -p sciencec produces a compiler whose build reports SC0400 naming the missing feature and the install command; cargo build -p sciencec --features llvm produces one that links LLVM-C and emits. That split is deliberate: a workspace nobody without LLVM can build is a workspace nobody can contribute to, and gating on a feature rather than on detection is the difference between a compiler that behaves the same on every machine and one that quietly differs depending on what happens to be installed.

What is measured, and what is not. The fourteen crates hold 1,910 #[test] functions at the commit this page was written against; a plain cargo test --workspace runs 1,796 of them, because a hundred and fourteen sit behind the llvm feature and that feature is off by default. There is no performance number anywhere on this page, because nothing has been benchmarked: the first performance target the project has written down lives in a design note and has never been run.

Scripts and programs#

A file's top-level statements, in source order, are the body of an implicit def main() -> Error?. That is the whole of script mode: there is no second file kind, no flag, and no module-initialisation phase.

def clip(value: Int, limit: Int) -> Int:
    if value > limit:
        limit
    else:
        value

# Statements and declarations interleave, and a statement may call a
# function declared below it.
let raw be 1_200
print(f"clipped to {clip(raw, 1_000)}")
# clipped to 1000

let low be clip(-5, 1_000)
print(f"and {low} passes through")
# and -5 passes through

Why the language has this at all. The people Science is for write a great many files that are ten lines long and run once, and a language that demands a main before it will print anything has put a ceremony between the user and the first correct result. The cost of admitting statements at the top level is a grammar decision that cannot be retrofitted — whether a file's top level is a sequence of declarations or a sequence of items and statements changes the parser, the resolver and every diagnostic that says "a module holds declarations only" — which is why it is settled in F0 although nothing else about the interactive tier is.

What a top level may hold, and how it was built

The production is one line long and it gained one alternative: top_level := item | stmt. An item is any of use, type, choice, interface, def, const, a Type has: block and a Type implements I line. A statement is the same Stmt the parser already produced for function bodies. No new statement kind, no new expression form, no new keyword and no new reserved word was added to buy this.

It ships as a desugaring, and that is worth knowing because it leaks in exactly one place. parse_module gathers the top-level statements and appends one generated def main() -> Error? whose body they are. No phase after the parser learns the word "script": the resolver, the type checker, MIR, region inference and codegen all see an ordinary function. The leak is that a generated node has no source text, so sciencec tools --json --all-functions on a script lists a main nobody wrote. It is pinned by a test rather than filtered, because filtering it out means teaching the driver about scripts, which is the one thing the desugaring buys out.

One line of the grammar needs two tokens to disambiguate. Both an implementation header and a statement may begin with an identifier. The rule is exact rather than heuristic: a top-level logical line beginning with an identifier is an implementation header if and only if the reserved word implements or has occurs in it at bracket depth zero before its : or its end. Neither word can occur in an expression, a path, a type or an assignment target, so this is one linear scan of one line with no backtracking and no speculative parse.

type Reading:
    channel: Int

Reading has:                          # an item: `has` at depth zero
    def first() -> Reading:
        Reading(channel: 1)

let r be Reading.first()              # a statement
let mutable n be r.channel
n be n + 40                           # a statement: assignment, no `has`

print(f"{r.channel} {n}")
# 1 41

The empty file is a program. A file with nothing in it, and a file holding only comments, both check clean and mean "do nothing, exit 0". There is no empty program diagnostic. The implementation consequence is smaller than it sounds and is stated here because it caught the back end: an empty script body produces no MIR body at all, so "falling off the end" is not a path any execution test can drive from Science source.

Statements run only in the entry file

Importing a module never runs anything: there is no module-initialisation phase, and a top-level statement in a file that something else uses is SC0213. The same file is a perfectly good script when it is the file you named, and a broken module the moment another file imports it, and the diagnostic shows both halves — the statement that would never run, and the use line that made it a module.

error[SC0213]: top-level statements in a module that is not the entry point
 --> clean.science:1:1
  |
1 | print("loaded")
  | ^^^^^^^^^^^^^^^ this would never run
  |
 --> plots.science:1:1
  |
1 | use clean (clean_up)
  | -------------------- `clean` is imported here, so it is a module, not a script
  |
  = note: Science does not run a module's statements when it is imported
  = note: move these statements into a function, or into the entry file

How the compiler tells a script body from a written main, given that no phase below the parser knows about scripts. It tests the one property the desugaring leaves behind: the generated main's name span is zero width, where a written one covers four bytes. A test pins that against a real parse, so if the parser ever gives the generated name a span, the test breaks rather than SC0213 quietly ceasing to fire.

Why the rule is strict rather than a warning. The alternatives were: run them once at first import, which is what Python, Ruby and Julia do and which makes use an effect — a line that can read a file, allocate or panic, invisibly, at its use site; do not run them and say nothing, which is the one thing a project whose UI tests compare diagnostics byte for byte should not choose; or warn, which data-io.md already dismissed by observing that SettingWithCopyWarning is a warning nobody reads. Either it matters or it does not. Relaxing this later — allow, do not run, warn — is source-compatible; tightening it later would not be.

A directory module needs no special case. mod.science is never an entry by rule two, which names main.science specifically, and it is reached by use whenever its directory is, so top-level statements in a mod.science are always SC0213.

Ordering, and the one direction that does not cross

There is no hoisting and no reordering. The statements run in source order. What is not ordered is declaration: a statement may call a function declared below it, because the resolver collects every definition in every module before it looks at a single body. By the time anything is resolved, everything is known, with no fixed point. The practical consequence for this audience is that a script's helper functions can go at the bottom, which is not true of MATLAB and not true of C.

The one thing that does not cross the line is the other way round: a named item does not close over the top level, so a def cannot see a top-level let. That asymmetry is enforced by construction — items are resolved in a scope the script bindings are not in — so the diagnostic reserved for it, SC0212, has never had anything to report and is not implemented. What you get is the ordinary not-found error:

error[SC0200]: cannot find `threshold` in this scope
 --> analysis.science:4:13
  |
4 |     value > threshold
  |             ^^^^^^^^^ not found

Three reasons the ban is there, and only the third is unobvious. It would make item bodies depend on execution order, so a function called before line 1 has run would read an uninitialised binding — C++'s static initialisation order fiasco, and Python's call-time NameError. It would put a hole in local inference, because one function's body would depend on another function's inferred local across a boundary drawn to keep that closed. And it inverts the region engine's analysis order into a genuine cycle: functions are analysed in reverse topological order of the call graph, callees before callers, so keep is analysed before the script body — but the binding's region is a fact about the script body's MIR. That is a dependency cycle across the call graph, which the strongly-connected-component fixed point does not cover, because it is not a call cycle.

A closure sees the top level; a named item does not. The closure is inside the script body, so its capture is an ordinary capture of an ordinary local and needs no rule of its own. That line is also what makes the F1 notebook tier tractable: because no item body can read a script binding, invalidating a cell invalidates statements downstream of it and never a function body — the dependency edges from cells go forward into cells and never sideways into items.

A top-level let binds a local of the script body, not a global and not a static. Its scope is the rest of the top level. It drops at the end of the script, in reverse declaration order, before the process exits — and a panic does not run drops, because panic is abort, so a panicking script leaves its temporary directory behind. Choosing a static instead would have bought exactly one thing, item bodies reading it, which the paragraph above already forbids for independent reasons; and it would have cost a 'static region, an at-exit registry with an order, and an initialisation-order analysis. All of the cost, none of the benefit.

public is an item modifier and a statement declares no name to export, so it is refused where a reader will first try it:

error[SC0107]: `public` has no meaning on a statement
 --> analysis.science:1:1
  |
1 | public let n be 1
  | ^^^^^^ a statement declares no name to export
  |
  = help: the statement runs either way: delete `public `

The exit-code contract

The script body's signature is def main() -> Error?, and that signature is the contract. There is no second mechanism, no sys.exit, and no status to return by hand. The signature is Error? rather than () because if err?: return err is the idiom for every fallible call, and a top level on which that idiom does not typecheck is a top level on which the language's own error model cannot be used. A script is mostly IO and IO is mostly fallible.

print("done")
return null
# done

$ sciencec build exit.science && ./exit.exe; echo "exit=$?"
done
exit=0

Three exactness notes, and all three are corrections the implementation forced. First: of the three spellings that give 0, return null is the only one that compiles. A bare return yields (), nothing turns () into null, and the result is the type error below. The sugar is decided and unwritten; implementing it is a coercion from () to Error? at a return. changing

error[SC0525]: expected `any Error?`, found `()`
 --> exit.science:2:1
  |
2 | return
  | ^^^^^^ this is `()`

Second: the failing row cannot be reached from any program this compiler can build. Error is an interface declared in the prelude, so Error? expands to (any Error)? and returning a non-null error means boxing a concrete error into an interface object — which allocates and fills a vtable, and this back end emits no vtables. The exit-1 path is emitted into every binary and tested by a harness that writes its own main to drive it, and it is unreachable from Science source. changing

Third: the script body's tail is always a generated null, never its last statement. Promoting a trailing expression to the tail, which is what block parsing does everywhere else, would make the value of print("hello") the script's return value — and () is not an Error?. "Falling off the end is an implicit return null" is spelled as that node rather than inferred.

Two things are deliberately absent and both would be one-line additions that cost a permanent name. There is no exit(code): the free function list is closed, and an exit code other than 0 or 1 has no caller yet. There is no argv: the process environment belongs to a library, not to the grammar. A leading #! line is a # comment and already lexes correctly; making it executable is a filesystem question and not a language one.

One main, or none

error[SC0117]: this file has top-level statements and also declares `main`
 --> both.science:2:5
  |
1 | let n be 1
  | ---------- the top-level statements start here, and are already a `main`
2 | def main():
  |     ^^^^ `main` is declared here
  |
  = note: a file whose top level holds statements is a script: the statements are the program, and the compiler writes the `main` that runs them
  = note: move the statements into `main`, or delete `main` and let the statements be the script

That diagnostic carries no applicable fix, and the absence is deliberate rather than an omission: there are two reasonable repairs and a compiler cannot choose between them. Everywhere a mechanical fix exists this compiler prints the exact replacement text; where two exist it prints neither, because a tool that applies the wrong one of two is worse than a tool that applies none. When it fires, the script body is not generated at all, so one mistake stays one diagnostic instead of cascading into every statement.

The three alternatives were priced and all three lose. Statements run, then main runs is Python's if __name__ == "__main__": wart with the condition made implicit instead of explicit, which is strictly worse, because at least Python's is visible in the source. main wins and the statements are module initialisation reintroduces the initialisation phase that the module rule above exists to delete. The statements win and main is dead is silently dead code. A file with a main and no top-level statements is of course fine, and is what a library's entry file looks like.

What names the entry, and what a crate is

Rule one: the file named on the command line. Rule two was to be main.science at the crate root when no file is named, and it is not built — it needs a crate root with no file to derive one from, which is the package manager's question. There is no sciencec run either; the commands are check, build, fmt, tools, ast, resolve and tokens.

A crate is one entry file plus the transitive closure of the modules its use declarations name, rooted at the entry file's directory. That definition is the implementation's; the design note that both rules lean on never defines the term. So sciencec check a.science b.science is two crates, one per name, and not one crate of two files — because each file named is an entry, and folding the command line into a single crate would make every file after the first a non-entry and report SC0213 on all of them. That is the opposite of what script mode is for.

$ sciencec check plots.science
error[SC0213]: top-level statements in a module that is not the entry point
1 error

$ sciencec check clean.science
$ echo "exit=$?"
exit=0

One consequence is worth stating because it has bitten a measurement: the same declaration in two files numbered in two orders used to produce two different const-expression normal forms, because the atom order was derived from a declaration id and ids are handed out in command-line order. That is fixed — the order comes from a canonical path now — and it is recorded in Types as the shape of the bug that a.science b.science can still cause elsewhere.

Bindings and literals#

let … be introduces a name. be on its own assigns to one that already exists. A binding is immutable unless it is declared mutable.

let title be "Regions"             # immutable, and the type is inferred
let mutable count be 0             # `mutable` is what makes assignment legal
let width: Int be 768              # the annotation is optional everywhere

count be 3                         # assignment: `be` without `let`
print(f"{title}: {count} runs at {width} columns")
# Regions: 3 runs at 768 columns

Every form of let, and the one that surprises people

mutable distributing over every name in a destructuring let is a decision, not an accident. The list receives one tuple, and a form in which half the names were mutable would need a second mutable in a position nothing else in the language puts one. So let mutable frame, err be read_csv(…) makes both frame and err assignable, which is almost always more than the caller wanted and is the cheaper of the two wrongs.

Shadowing is allowed, and the right-hand side sees the old binding. A second let with the same name in the same scope introduces a new binding rather than assigning to the old one, and the initialiser is evaluated before the new name is in scope, so let n be n + 10 reads the previous n. This is the Rust rule and not the Python one; in Python there is no second binding to make, only a rebinding.

let n be 1
let n be 2                         # a second binding, not an assignment
print(f"{n}")
# 2

let n be n + 10                    # the `n` on the right is the one above
print(f"{n}")
# 12

Immutable is the default, and this is the first real cost of the language. In NumPy every name is rebindable and every array is mutable, and nothing asks which you meant. Here the compiler asks once, at the binding, and in exchange a reader of let title be … knows without searching the function that no line below changes it. The word is mutable and not mut because abbreviated keywords lose an argument the language still holds to: count the spelling across Fortran, MATLAB, R, Julia, Python, JavaScript and PHP before shortening a word — not across the corpus a model was trained on.

This is enforced, and until recently it was not. The word lexed, parsed, resolved and arrived at the binding — where nothing ever read it. The program below used to check, build, link, run and print 3. It is now SC0304, and the note carries the one-word fix.

let count be 0                     # no `mutable`
count be 3                         # SC0304: `count` is not mutable
print(f"{count}")

error[SC0304]: `count` is not mutable
 --> counter.science:2:1
  |
1 | let count be 0
  |     ----- declared here, without `mutable`
2 | count be 3
  | ^^^^^ assigned here
  |
  = note: declare it `let mutable count`

The rule stops at the first borrow, and that is the half worth stating. def bump(counter: mutable borrowed I64) writing counter be counter + 1 is not reassigning counter; it is writing the referent, which is what mutable borrowed exists to permit. So the walk from the target toward its root stops as soon as it crosses a borrow, and from there the borrow rules govern rather than this one — including when the reference is reached through a binding that is itself immutable, because the storage written belongs to the referent and no binding in that body owns it.

Two constructs are not yet caught, and the reason is the same for both. The rule reads types, so it runs after inference writes back, and where a type still did not come out it stays silent rather than guess. A range carries no type at all — there is no Range in the prelude, which is the same absence SC0538 reports — so for i in 0..3: cannot be told its i is not mutable, although for mutable i in 0..3: parses and checks. A method on a prelude type is not looked up either, so a binding initialised from one has no type to read. changing

Assignment, and the two spellings that do not exist

Assignment is a statement, not an expression. It has no rung on the precedence ladder and produces no value, so if (x be 1): is not something the grammar can express. There is also no compound assignment: count be count + 1 and never count += 1. One spelling instead of two, and a rebinding inside a loop stays visible on the line where it happens.

error[SC0105]: expected an expression, found `=`
 --> loop.science:2:8
  |
2 | count += 1
  |        ^ expected an expression, found `=`

error[SC0100]: expected end of line, found a number literal
 --> loop.science:2:10
  |
2 | count += 1
  |          ^ expected end of line, found a number literal

Two errors rather than one, because += lexes as + then = and there is no = token in the language at all — the parser recovers past the + and then meets the literal. This is the one place on the page where the one-mistake-one-message rule is not met, and it is not met because the lexer has no compound-assignment token to recognise the habit with.

Assignment to a name that was never bound is an ordinary resolution error, which is worth knowing because it is the failure mode of a typo in a long script: other be 2 with no let other above it is SC0200, cannot find other in this scope — not a new binding, the way it would be in Python.

That said: count be count + 1 checks and does not build. An assignment whose right-hand side reads a local arrives at the back end untyped and is refused, where let next be count + 1 is emitted without complaint. It is a gap in the lowering rather than a rule, and it is stated here because it is the shape of the most ordinary line in a loop. changing

error[SC0400]: this `sciencec` cannot build a value the front end left untyped: its `Ty` is `TyKind::Error` and no diagnostic was reported for it. The three this compiler has met are a call to `print` or `write`, whose signatures `science-resolve`'s `builtins.rs` withdrew; a `for` loop's range and iterator temporaries; and a discriminant temporary, which is handled rather than refused

Literals

let decimal be 1_000_000
let hex be 0xdead_beef
let octal be 0o777
let binary be 0b1010

let pi be 3.14
let tiny be 1e-9
let single be 2.5f32

let greeting be "hola"
let letter be 'a'
let flag be true
let missing: Int? be null          # absence, and the only spelling for it

print(f"{decimal} {hex} {octal} {binary}")
print(f"{pi} {tiny} {single}")
print(f"{greeting} {letter} {flag} {missing?}")
# 1000000 3735928559 511 10
# 3.14 1e-9 2.5
# hola a true false

The last line is worth pausing on: {missing?} prints false, not null. ? is a presence test that produces a Bool; it never unwraps. That is the single most misread character in the language and Errors is where it is argued.

Every numeric literal takes _ anywhere between digits, in every base, and the same character is the grouping separator the format mini-language adds to Python's, so a number a program prints pastes back into one. A literal with no suffix defaults to Int if it has no point and Float if it has one — but only if nothing constrains it: an unsuffixed literal is inferred first and defaulted only as a last step, because a language that silently makes 1 an I32 will be wrong on somebody's index arithmetic. The suffix forms are the type name in lower case: 42i32, 255u8, 2.5f32.

There are no negative numeric literals. -1 lexes as the operator - applied to 1. In expression position nothing turns on it; in type position it is the reason a const argument needed a signed integer node before unit exponents could be written at all.

const WIDTH be 768                  # a compile-time constant
type Embedding is Array of F32      # a type alias

let escaped be "a\tb\nc \u{1F600}"  # the whole escape list, plus \r \\ \" \' \0
let raw be r"C:\runs\2026\peaks.csv"
let sized be 42i32
let nothing be ()                   # the empty tuple: a value, not an absence
let vector: Embedding be (Array of F32).new()

print(escaped)

This block checks and does not build, and the two reasons are worth knowing: a const read as a value has no lowering — it reaches the back end untyped and is refused with the SC0400 above — and neither has an Array. It is here because the forms are the language's and the reader needs them; the output is absent because inventing it would be the one thing this page must not do.

const is the one inherited abbreviation in the language, and the register of shortened keywords names it beside def. It is a compile-time constant rather than a read-only binding: it is substituted where it is used, and it may stand as a const-generic argument, which a let may not. A const is also the only thing an item body may read from something written at module level, which is why the diagnostic for a function reaching for a script binding suggests turning it into one.

Escapes, and what is in the list

The escape list is \n \t \r \\ \" \' \0 \u{…} and nothing else. There are no block comments, no triple-quoted strings, no \x41, no octal escape and no \e. \u{…} takes one to six hexadecimal digits and encodes the scalar as UTF-8, so \u{1F600} is four bytes. \0 is a NUL byte in the middle of a string and does not terminate it — a Science String carries a length.

let escaped be "a\tb\nc \u{1F600}"
let more be "\r|\\|\"|\'|\0|"
let raw be r"C:\runs\2026\peaks.csv"

print(escaped)
print(more)
print(raw)

Piped through cat -A, so that the bytes that do not print are visible: ^I is the tab, ^M the carriage return, ^@ the NUL, $ the end of each line, and the four M- bytes the UTF-8 encoding of one emoji.

$ sciencec build escapes.science && ./escapes.exe | cat -A
a^Ib$
c M-pM-^_M-^XM-^@$
^M|\|"|'|^@|$
C:\runs\2026\peaks.csv$

Anything else after a backslash is refused at the character, by the lexer, with the whole list in the note — which is the cheapest possible way to teach a closed set:

error[SC0006]: unknown escape sequence `\q`
 --> text.science:1:9
  |
1 | print("a\qb")
  |         ^^ unknown escape
  |
  = note: the escapes are `\n`, `\t`, `\r`, `\\`, `\"`, `\'`, `\0` and `\u{...}`

Numbers

Numeric types are written out and never converted implicitly. I8 … I64, U8 … U64, F16, BF16, F32, F64, with Int aliasing I64 and Float aliasing F64. as is always written, including where it loses precision, because a language that silently widens an F32 to an F64 has made a decision about your memory budget that you did not ask for.

Four numeric behaviours are decided here rather than left open, because a numeric language cannot leave them open. Integer overflow panics in debug builds and wraps in release. Integer division truncates toward zero and % takes the sign of the dividend. as from float to integer saturates, and NaN becomes zero. And F32 and F64 implement Eq but not Ord, because NaN has no total order — so sorting floats takes an explicit total-order function rather than silently producing a permutation that depends on where the NaNs started. Reductions have a defined order unless they are marked unordered, and a result that differs between runs is opt-in, because this is a language whose users publish.

One of those four is emitted, and the others are not. Saturating float-to-integer casts work in both directions and on NaN. Integer / and % are refused by the back end entirely, and so are shifts. Overflow does not panic: it wraps, and there is no build in which it does otherwise, because there are no build profiles yet for "debug" to name. changing

print(f"{1.0e30 as I32}")
print(f"{-1.0e30 as I32}")
print(f"{(0.0 / 0.0) as I32}")
# 2147483647
# -2147483648
# 0

let big be 2147483647i32
print(f"{big + 1i32}")
# -2147483648

let u be 255u8
print(f"{u + 1u8}")
# 0

Note that 0.0 / 0.0 is a float division and is emitted; it is integer / that is not. The two refusals name their reasons, and both reasons are the same shape — a check nothing above the back end emits:

error[SC0400]: this `sciencec` cannot build integer `/` or `%`, whose divide-by-zero check nothing above this crate emits — `IntOp`'s own note calls it "a panic the caller has already guarded" and no caller does, and a bare `sdiv` is undefined at zero rather than a trap

error[SC0400]: this `sciencec` cannot build a shift, whose amount nothing above this crate bounds — a shift by at least the operand's width is poison in LLVM and neither the mask nor the panic that would stop it is specified

null, (), and names you may not bind

null is a literal like true and false: its spelling is fixed, so a program may not bind the name. It inhabits a nullable type T? and nothing else. () above is the empty tuple, which is a value and not an absence — a function with no return type returns it, and a body whose last expression is not () in such a function is a type error rather than a discarded value.

Some names a scientist will reach for are reserved for a phase that does not exist yet, and the error arrives in binding position. shape, model, tensor, union, mod, yield, kernel, import, assert, with, move, on, static, pure, parallel, macro, extern and unsafe are the list, and Reference tables keeps it current. Deliberately not reserved, for the same audience reason: grad, dim, dims, axis, device, dtype, unit, alias — and function, which left the keyword list when def arrived and is an ordinary identifier now.

error[SC0102]: expected an identifier, found `model`, which is reserved for a later phase
 --> train.science:1:5
  |
1 | let model be 1
  |     ^^^^^ expected an identifier, found `model`, which is reserved for a later phase

A design note argues that most of that list should be freed and the compiler has not acted on it yet. Its central proposal is the dot rule: after a . there is nothing a name could be confused with, because a member name is the only construct the grammar admits in that position, so any word should be accepted there. It is not implemented, and the consequence is that x.shape — the single most common attribute access in numerical Python — produces the error above twice, once for the member name and once for the line that could not continue. The note also records that the reservation protects a construct F1 turns out not to want. Where the note and the compiler disagree, this page documents the compiler. changing

Strings and formatting#

There are three string literal kinds and they do not combine. A plain "…" processes escapes. An f"…" also interpolates. An r"…" does neither.

let channel be 3
let flux be 0.1 + 0.2

print(f"channel {channel}")
print(f"flux {flux}")
print(f"{channel} squared is {channel * channel}")
print(f"a literal brace: {{{channel}}}")
print("{channel} is four words of text, not a hole")
# channel 3
# flux 0.30000000000000004
# 3 squared is 9
# a literal brace: {3}
# {channel} is four words of text, not a hole

The second line is not a bug and it is not a rounding choice. A float with no format code prints the shortest decimal string that reads back as the same float, so 0.1 + 0.2 prints what it is. A language for people who publish numbers does not get to round in the default path: the rounding is {flux:.3}, written where the author decided it, and the default tells the truth.

The rest of the default rendering is decided too, and for the same reason. NaN, inf and -inf are spelled exactly that way, honouring width and alignment and ignoring precision — not nan, and not NaN%. -0.0 prints as -0.0, because it is a different float and hiding that has cost people days. Bool prints true and false, matching the literals. Default alignment is left for strings and right for numbers, which is Python's rule and the one that makes a column of numbers a column.

Why the f is required. The alternative is Python's, where every string is a candidate and a brace must be doubled everywhere. This audience writes JSON, LaTeX and regular expressions, all three of which are made of braces, so the cost of interpolating by default lands on exactly the strings these users have most of. Under that design "\\frac{a}{b}", in a file that happens to bind a and b, would silently interpolate — a wrong answer produced quietly, which is the failure this project exists to remove. Swift's \(x) was the clever third option, because \ already had to be escaped and so steals nothing where a brace steals a great deal; it loses on recognition, since f"…" is what a pandas user already types.

With the prefix, "{}" is two characters of text and needs nothing. The lexer pays for it by lexing the interior properly rather than scanning for a closing quote, and one consequence falls out for free: nested string literals, including a nested f"…", are admitted to any depth.

let name be "A12"
let channels be 768

print(f"{f"{name}"} has {channels}")
print(f"{f"{f"{name}"}"}")
# A12 has 768
# A12

What that costs the lexer, stated because it is the largest single piece of work in the design. f"{m["a"]}" contains a " that does not end the literal, and f"{f"{x}"}" contains braces that are not the match, so the lexer is a machine with a mode stack rather than a scanner: f" pushes a string frame, { pushes an expression frame, a } at brace depth zero pops it, and a " inside an expression frame pushes another string frame. The indentation machine is suspended inside an interpolation, exactly as it already is inside unclosed brackets — that rule now has a second trigger. Rust avoids all of this by making format! a macro over a literal, which Science cannot do because it reserves macros without implementing them. Swift, Kotlin, JavaScript and now Python all pay exactly this cost. It is paid once.

What may go in a hole, and the four ways it is refused

An expression, with three restrictions. It is an expression and not a statement, so no let, no return, no break. It may not span a line. It may not contain a # comment, which would swallow the closing brace and the quote. The alternative considered was admitting bare names only, and it was rejected on a teaching argument: a rule that admits {mu} and refuses {frame.length()} teaches a boundary a user meets within minutes and cannot predict, and half a feature here is worse than none. That is also the boundary Python shipped in 3.6 and spent until PEP 701 in 3.12 climbing out of.

error[SC0170]: this interpolation has no closing `}`
 --> report.science:2:9
  |
2 | print(f"{n")
  |         ^ this `{` opens an interpolation
  |           - the literal ends here
  |
  = note: inside an `f"…"` a literal brace is written `{{`

error[SC0174]: an interpolation with nothing in it
 --> report.science:2:9
  |
2 | print(f"{}")
  |         ^^ name the value
  |
  = note: there are no positional fields: `print` takes one value, so `{}` has no argument list to refer to

error[SC0175]: a `#` comment inside an interpolation
 --> report.science:2:12
  |
2 | print(f"{n # c}")
  |            ^ this would comment out the rest of the literal
  |
  = note: an interpolation holds one expression: no `let`, no statement, no comment and no line break

One of the five does not hold the one-mistake-one-message line. A let inside a hole is reported as SC0105, expected an expression, found let, and then cascades into three more as the parser walks out of the literal and off the end of the call. SC0175's note names let and statements among the things it covers; the code that actually fires for them is the generic one. A missing } likewise leaves the mode stack deep and produces a second error from the call. Error recovery inside an interpolation is the weakest joint in this part of the lexer, and the design says so in advance. changing

An interpolation does not consume its operands: f"{doc}" leaves doc usable. That is the guarantee; the mechanism is two rules rather than one, and the design's own amendment corrects itself on the point. Six of the seven runtime entry points that render a hole take their argument in a register — an Int, a U64, an F64, an F32, a Bool, a Char — so what happens there is a read of a Copy type, not a loan. Only a String is passed through a pointer, and that one case is a borrow in the mechanical sense.

What an f"…" costs. Its type is String and it lowers to a builder over the literal fragments. The design specified one allocation, with the capacity precomputed from the fragments plus a per-type estimate for each hole — and the capacity has nowhere to go: the runtime has fifty-four entry points and not one of them takes a capacity. So the accumulator starts at the growth floor and the common case is one allocation per growth. The permitted elision, where an f-string handed straight to print renders into the sink instead of building a String, is opt-in by its own wording and this implementation has not opted in. Both facts are worth stating as a class: a note may specify a cost its own interface makes unreachable, and only an implementation finds that out. changing

A plain string literal that contains what would be a valid interpolation — every name inside it resolving in the enclosing scope — is specified as SC0172, a warning carrying two applicable fixes: insert the f, or double the braces. It is not implemented, and the lexer's own note says why it cannot be: deciding whether every name inside a string resolves is a question about scope, and the lexer has none. The suppression is r"…", which the lint never inspects — and the known false positive is LaTeX, where "\\frac{a}{b}" beside bindings named a and b will fire. changing

The three kinds do not combine, and asking for a fourth is named rather than guessed at:

error[SC0177]: `rf"…"` is not a string literal
 --> report.science:2:7
  |
2 | print(rf"{n}")
  |       ^^ the literal prefixes do not combine
  |
  = note: there are exactly three literal kinds: `"…"` is text, `f"…"` interpolates, and `r"…"` processes no escapes. A raw interpolating string is a fourth set of rules for a case nobody has demonstrated

r"…" has no way to contain a ", and that is the stated price of not adopting Rust's r#"…"#. The extension is known and it is source-compatible to add. A string that needs escape processing and contains a quote is an ordinary "…" with \\. f and r do not become reserved words: calls are always parenthesised and there is no juxtaposition operator, so f"x" can only be a prefixed literal and never f applied to "x". let f be 1 and let r be radius both remain legal.

There is no multi-line string literal and the omission is deliberate rather than pending: r"…" covers LaTeX and regular expressions, and a triple-quoted form would have to decide its interaction with both prefixes and with indentation stripping before it could be added. A SQL query or an embedded shader will want one, and that is when the decision gets made.

The format mini-language, and the part of it that exists

The specified spec is Python's mini-language with four things removed and one added. A conversion flag precedes the colon and selects the interface; everything after the colon selects the rendering.

conversion := '!' ('i' | 's')

spec       := [[fill] align] [sign] ['#'] ['0'] [width] [grouping]
              ['.' precision] [code]
align      := '<' | '>' | '^'
sign       := '+' | '-' | ' '
grouping   := ',' | '_'
width      := integer | '{' expression '}'
precision  := integer | '{' expression '}'
code       := 'f' | 'e' | 'E' | 'g' | 'G' | '%' | 'd' | 'x' | 'X' | 'o' | 'b' | 's'

g is the code a scientist should reach for most. .3g is three significant figures whatever the magnitude, which is what reporting three sig figs means and what .3f does not do. The one addition over Python's set is _ as a grouping character beside ,, so that a number a program prints pastes back into one. # is the alternate form: the 0x, 0o and 0b prefixes, and a retained decimal point at precision zero. A 0 before the width means zero-fill and sets alignment to right, so f"{i:04d}" is 0007.

The spec is checked against the static type at compile time, which is the decision that makes the rest of it work: {n:.3f} on an integer is a compile error and not a surprise at run time, eight hours into a training run, on the logging line. The legality table is short — float codes want a float or a DisplayNumber; integer codes want an integer; a precision wants a float code or a String, where it means truncation; # wants x X o b f e g; grouping wants a numeric code — and everything else is SC0274.

It costs four things and the design names them. A format spec is no longer a value: there is no format(fmt, x) taking a String, and a program that must choose between f and e at run time writes the if. A typo in a spec becomes a hard error in an interactive tier, where a bad spec will stop a cell rather than print something wrong. The type checker acquires a small parser that must produce spans into the middle of a string literal. And DisplayNumber has to exist, because without it f"{q:.2f}" on a Quantity would be an error.

The one dynamic hole: width and precision may themselves be Int interpolations. The code stays static. f"{row.value:>10.{digits}f}" preserves the whole of the check, because the part that can be wrong — which rendering — is still a literal, and the part that became dynamic is a number, which cannot be the wrong kind of thing.

Four things were removed from Python's mini-language. n, the locale-aware code, is rejected outright: locale-dependent output means the same program prints 3.14 on one machine and 3,14 on another, which breaks every downstream parser and every reproducibility claim the language makes. Positional and implicit fields go because print is unary and there is no argument list to be positional in. !r and !a go because !i covers the first and the second is a Python-2 artefact. And attribute and index access in the spec go because the expression side already has them. The consequence nobody gets back is localisation: a program that must print 3,14 for a Spanish-language report has no facility, and the right shape for one is an explicit Locale value passed to a formatting call.

None of the mini-language is built. f"{value}" is the whole of what this compiler reads, and any spec at all — including the !i conversion — is SC0173, which is the good failure: it names the feature as unbuilt rather than accepting the spec and ignoring it. changing

error[SC0173]: a format specification, which this compiler does not implement
 --> report.science:2:12
  |
2 | print(f"{pi:.3}")
  |            ^^^ no part of the format mini-language is built
  |
  = note: `f"{value}"` is the whole of what this compiler reads: an expression, rendered by its `Display`. The fill, alignment, sign, width, grouping, precision and type codes, and the `!i` conversion, are specified and unbuilt

Display, Inspect, and what a hole requires

A plain hole renders its value through Display, which is the spelling a person reads. {x!i} renders through Inspect, which is the spelling a program reads — print(f"{name}") gives A12 and print(f"{name!i}") gives "A12", quotes included. The division matters most for units, where Display prints the typeset m/s² and Inspect prints 9.80665<m/s^2>, which pastes back into a program unchanged.

Both take a Formatter, and that is what lets a user type honour a spec at all. The receiver is self, the shared borrow, and that is where the does-not-consume guarantee comes from. Neither Formatter nor FormatSpec is in the prelude, so the block below is the specification and not a listing — writing it in a file gives SC0200, cannot find Formatter in this scope. What a program can write today is an implements Display: block with whatever method shape it likes, because nothing checks a block against its interface. changing

interface Display:
    def display(self, into: mutable borrowed Formatter)

interface Inspect:
    def inspect(self, into: mutable borrowed Formatter)

Formatter has:
    def text(mutable self, value: borrowed String)    # pads, per the spec
    def raw(mutable self, value: borrowed String)     # does not pad
    def number(mutable self, value: F64)
    def integer(mutable self, value: I64)
    def spec(self) -> FormatSpec

FormatSpec is a plain record of nullable fields — fill, align, sign, width, precision, code, alternate, grouping — for an implementation that needs to branch on it. DisplayNumber is a marker with no methods that grants a type the numeric codes; it says they are meaningful for the type and cannot prove the implementation honours them. The check is type-level and that is where it stops.

Why !i and not Rust's {x:?}. This is the one place Science must not copy Rust, and the reason is one character wide: ? is already the presence test, so f"{err?}" prints true — the error is present — and f"{err:?}" would print the error itself. One colon apart, one a Bool and the other the value. That is not a collision a language should ship. !i also leaves {x!i:>20} well-formed, which {x:?>20} never was in Rust either.

Three things deliberately do not implement Display, and meeting them is how a reader learns the rule. A T? does not, until it is narrowed — printing a possibly-null value must be a decision, because a silent null or an empty cell in a published table is the failure this prevents. Arrays and maps do not; they implement Inspect, because there is no one right way to show a million rows to a person and there is exactly one right way to show them to a debugger. Closures and function values implement neither.

error[SC0275]: `Doc` cannot be interpolated: it does not implement `Display`
 --> report.science:5:10
  |
5 | print(f"{d}")
  |          ^ this is `Doc`
  |
  = note: an interpolation renders its value through `Display`. A nullable does not implement it until it is narrowed, and a value that implements nothing needs an `implements Display:` block before it can be printed

Inspect without derivation is a dead letter and the design says so: {x!i} will work on library types and fail on the user's own, which is the worst possible distribution, because it is the user's own types they are debugging. It is a second customer for whatever eventually resolves the macro boundary. The other thing worth knowing is that every Inspect rendering is part of the spec: the UI tests compare rendered diagnostics byte for byte, and diagnostics print values, so changing how a Map inspects is a spec change.

print is unary, and there are four output functions

stdout's policy is C's, and every tool in a pipeline assumes it. stderr is unbuffered because a message that precedes a crash must survive the crash. Ordering between the two streams is not guaranteed when one is redirected and the other is not. The rule of thumb is results to stdout, progress and warnings to stderr — a program whose stdout is a CSV must be able to show progress without corrupting it, and that is the only reason print_error exists at all.

print takes one value. Not two, not none. A blank line is print(""). Three reasons in increasing weight: a variadic print is a second spelling of f"{a} {b}"; the separator it would insert is a hidden rule somebody has to look up — print("rows:", n) gives one space and print("rows: ", n) gives two; and — decisively — Science has no variadic functions and should not acquire them for one call. Formatting belongs in the string, where it is visible.

error[SC0275]: `print` takes one value
 --> report.science:3:1
  |
3 | print(a, b)
  | ^^^^^^^^^^^ 2 arguments were supplied
  |
  = note: interpolate instead: `print(f"… {value}")`

Of those five, the prelude declares three. print, write and panic resolve; print_error and write_error do not, and calling one is SC0200, cannot find print_error in this scope. That is deliberate and it is the better failure: a name that resolves with no runtime entry point behind it is checked in silence and refused at the end of the build, which tells the user nothing at the place they can act on it. The two names are absent because the runtime has no entry point for them, not because the namespace is crowded. changing

Of the three that resolve, one builds. print is emitted. write and panic resolve, check, and are refused by the back end with SC0400, a call to write, which this crate was given no MIR body for. So every listing on this page that produces output produces it through print, and there is no program yet that can demonstrate a panic message. changing

print's argument type is declared nowhere. The design gives it borrowed any Display; writing that signature was measured and withdrawn, because it turns every print(x) into a borrow-and-unsize into an interface object, and this back end emits no vtables — so declaring it correctly makes every print in every program unbuildable. What ships is the half that costs nothing: the arity is checked, the type is not, and print(doc) on a type with no Display is accepted by check and refused by build. That is the worse place to find out and the decision says so. changing

error[SC0301]: use of a moved value
 --> twice.science:6:10
  |
5 | let a be consume(s)
  |          ---------- `s` is moved here
6 | let b be consume(s)
  |          ^^^^^^^^^^ ...and moved again here, after the move
  |
  = note: every value has one owner, and assigning, passing or returning it transfers that owner (§6.1 rules 1 and 2), so the name is empty afterwards (rule 3)
  = note: borrow at the earlier use instead of moving, or give the second use a value of its own; a type that is not `Copy` is never copied implicitly

error[SC0402]: the linker failed
  = note: the command was: (the backend, before the linker)
  = note: what follows is the linker's own output, verbatim:
  = note: the module failed verification in `<module>`: Call parameter type does not match function signature!
 %v11 = load [2 x i64], ptr %1, align 8
 i64  call void @science_string_push_i64(ptr %v10, [2 x i64] %v11)

Unicode, and where the line is drawn

Unicode letters are legal in identifiers. σ, Δt, μ and χ2 are names. The boundary is the Unicode category and not taste: χ2 and not χ², because a superscript two is a number rather than a letter, and neither are ∇, ∂ or ℏ, which are symbols. Identifiers are normalised to NFC when they are lexed — one call in the lexer, and without it é as one scalar and é as e plus a combining accent are two different identifiers rendering identically. A single identifier that mixes scripts is SC0015, a warning — on mixing within one name, because Α, А and A are three different characters that look the same, so σ alone and σ_max are both fine.

≤, ≥, ≠, ∑, √, × and their relatives are not operators and are not accepted as aliases for anything. <= is the only spelling of <=. The design concedes the strongest counter-argument rather than hiding it: ≤ to <= is mechanically canonicalisable by a formatter, so the "permanent drift" argument that killed the word forms of the comparisons does not transfer here, and pretending it does would be dishonest. What is left is three things: an input problem, since no standard keyboard produces ≤; homoglyphs, which are worse — U+2212 MINUS SIGN is not -, U+2215 DIVISION SLASH is not /, and every one of those arrives by paste from a PDF; and the observation that ∑ is not an operator at all but a binder with a bound variable, an index range and a body, so what you would actually get is ∑(xs), a function call wearing a costume, where xs.sum() already exists. The recommendation if it is ever revisited is editor-side rendering: the file contains <= and the editor displays ≤.

Doc comments are ##, and there is no docstring

A documentation comment is a run of ## lines immediately preceding a declaration — a module, a function, a type, a choice, an interface, a const, a type alias, a field, a variant, an interface member or an implements block. The first line, up to the first blank ##, is the summary; the content is Markdown; there are no @param tags, because the parameter names and types are in the signature and a tag that restates them is a second copy that goes stale.

## Spectral preprocessing.
##
## Everything here assumes the dark current has been subtracted.

## A single detector reading.
type Row:
    ## Instrument identifier, as written in the run log.
    station: String
    ## Channel count. Always 768; this is checked on load.
    channels: Int

## What went wrong while reading a run.
choice LoadError:
    ## The file had a channel count other than 768.
    WrongChannelCount(Int)
    ## The file was unreadable or absent.
    Unreadable(String)

Why not """…""". Most things that need documentation have no body — a field, a variant, a const, an alias, a module — so a docstring form covers functions and then needs a second form for everything else. It would require adding a triple-quoted literal, with its own indentation rule to argue about forever. And a docstring in the body is a value in Python and would be a lie here: an expression statement with no effect that the compiler silently treats as metadata. ## also composes correctly with # — a # TODO beside a doc comment stays an ordinary comment, a distinction a docstring form cannot make at all. There is one sigil and no module-level second one, because modules are files and position is unambiguous.

What they cost: nothing at run time. The lexer keeps ## runs as trivia attached to the following token, the parser attaches them to the node, and they survive into HIR — and that much must happen in F0, because once the lexer discards them every tool downstream is built assuming they are gone. sciencec emits them into a metadata section of the object file: a string table plus an index from fully-qualified name to offset, static data, not reachable from any code path, strippable.

A ## run attached to nothing — at the end of a file, or separated from the next declaration by a blank line — is specified as SC0176, a warning with the fix make it #. It is not implemented: a stray ## run checks clean and silently documents nothing, which is precisely the silent failure mode the diagnostic exists to prevent. changing

Doc tests are specified and are F1. A fenced science block inside a ## run is compiled and run; science,no_run is compiled only; science,fails must fail and the tool checks the diagnostic code; and a neighbouring output fence is compared to stdout byte for byte, which makes a doc comment a test of the formatting too. The reason it matters more here than elsewhere: Science has no training corpus, so the material a model will learn this language from is its documentation — and doc tests are what make it impossible for that documentation to contain an example that does not compile. The same argument is why this page extracts and checks its own listings.

Types#

A record is a type. A sum type is a choice. Both take generic parameters with of, and a generic parameter may be a type or a constant.

type Reading:
    channel: Int
    counts: Int

choice Format:
    Plain
    Markdown
    Json

choice Measure:
    Unknown
    Exact(Int)
    Range(Int, Int)

def width_of(m: Measure) -> Int:
    match m:
        Unknown: 0
        Exact(v): v
        Range(low, high): high - low

def label(f: Format) -> String:
    match f:
        Plain: "plain"
        Markdown: "markdown"
        Json: "json"

let r be Reading(counts: 4_900, channel: 1)   # named, and in any order
print(f"{label(Json)} {r.channel} {width_of(Range(3, 11))}")
# json 1 8

Every declaration form

A record is constructed with named fields, always, and in any order. Reading(counts: 4_900, channel: 1) above puts them backwards and means the same thing. There is no positional record constructor, so there is no question about what the second argument is, and reordering a declaration's fields cannot silently change a call site. The same syntax is not a way to call a function — named arguments build a record and nothing else:

error[SC0206]: named arguments build a record, but `f` is a function
 --> call.science:4:10
  |
1 | def f(x: Int, y: Int) -> Int:
  |     - defined here
...
4 | let a be f(x: 1, y: 2)
  |          ^ not a record type

A choice variant's payload is positional and is matched by position, which is the one place in the language where the order of a declaration's parts is load-bearing. A variant is constructed by naming it — bare when it has no payload, Range(3, 11) when it has — and it may be written qualified, Format.Json, or bare, Json, where the type is known.

A choice is closed, and closing it is the point

A match over a Format must handle every variant, so adding Latex to the declaration breaks every place in the program that decided what to do with a format — loudly, at compile time, with the missing patterns listed. That is the opposite of a string constant or an integer flag, where adding a fourth value breaks nothing and is discovered by a wrong answer. It is also what lets a tool schema turn a choice into a JSON enum with nothing written by hand.

error[SC0250]: `Format` has values no arm of this `match` covers: `Markdown`, `Json`
 --> label.science:7:11
  |
7 |     match f:
  |           ^ this is `Format`
  |
  = note: a `match` answers for every value or the program has no answer for the rest (§4.5); write an arm for `Markdown` — or a `_` arm, which covers everything the arms above leave

The algorithm is Maranget's, which is what rustc uses, so the message reports a concrete witness — the shape of a value no arm covers — rather than the word "non-exhaustive". A nullable participates as an ordinary constructor: matching null plus the non-null case over a Doc? is exhaustive. A repeated variant name in the declaration is caught first, by the resolver:

error[SC0201]: the variant `Plain` is defined more than once
 --> format.science:3:5
  |
2 |     Plain
  |     ----- first defined here
3 |     Plain
  |     ^^^^^ defined again here

choice LoadError:
    NotFound(String)

# No `implements Error` line, and the position test catches it anyway.
def load(path: borrowed String) -> (Int, LoadError?):
    (0, LoadError.NotFound("x"))

def read() -> Int:
    let value, err be load("a.toml")
    if err?:
        return 0
    value

error[SC0140]: `err` is never checked for an error
 --> load.science:8:16
  |
8 |     let value, err be load("a.toml")
  |                ^^^ bound here and never tested
  |
  = note: test it with `if err?:`, pass it on, or return it — or rename it to `_err` to say the failure is deliberately ignored

Recursion, Box, and the check that is missing

Box of T is a heap indirection, and it is why a choice can name itself. A recursive record with no indirection has no finite size, and Science asks you to write the box rather than inserting one, because where the indirection sits is a performance decision in a language whose users care about memory layout.

choice Tree:
    Leaf(Int)
    Node(Box of Tree, Box of Tree)

Nothing enforces it. A choice whose variant holds itself directly, and a type whose field is its own declaring type, both check clean today — there is no occurs check over the declaration graph and no infinite-size diagnostic. It is a layout error the back end would have to meet, and it does not, because nothing that reaches the back end has ever had one. Write the Box; the compiler is not going to remind you. changing

choice Tree:                    # no `Box`, and this checks clean
    Leaf(Int)
    Node(Tree, Tree)

type Node:                      # so does this
    next: Node

Generic arguments, and where the parentheses go

type Doc:
    title: String

def one(items: Array of Doc) -> Int:            # one argument needs no parentheses
    items.length()

def two(index: Map of (String, Int)) -> Int:    # two or more do
    index.length()

def nested(groups: Array of (Map of (String, Int))) -> Int:
    groups.length()

def build() -> Array of Doc:
    (Array of Doc).new()                        # an associated call needs its own parens

This is not a style rule; it is the grammar. Array of Doc parses because a single type argument cannot contain a top-level comma, so the next comma ends it. Map of String, Int in a parameter list genuinely cannot be parsed — that Int could be Map's second argument or the function's second parameter, and no amount of lookahead decides which, because both readings are well-formed. So several arguments take parentheses, and nesting follows the same rule for the same reason. What you get is the parser running out of parameter list:

error[SC0100]: expected `:`, found `)`
 --> index.science:1:34
  |
1 | def two(index: Map of String, Int) -> Int:
  |                                  ^ expected `:`, found `)`

Array of Doc.new() is ambiguous in the same family: does .new() attach to Doc or to the whole generic type? Science requires (Array of Doc).new(). The alternative considered was making the space in Array of Doc .new() significant, which would make whitespace load-bearing in a way nothing else in the language is. The form is ugly and it is rare, and the compiler names it rather than producing a confusing downstream error:

error[SC0116]: `.new()` could belong to `Doc` or to `Array of Doc`
 --> build.science:5:5
  |
5 |     Array of Doc.new()
  |     ^^^^^^^^^^^^^^^^ this associated function call is ambiguous
  |
  = note: Science reads it as `(Array of Doc).new()`, the whole generic type
  = help: write the parentheses to say so: `(Array of Doc)`

Generic arity is not checked. Pair of Int where Pair takes two parameters, and Doc of Int where Doc takes none, both pass check in silence. The resolver admits a const parameter in a type position because there is no way to tell the two apart without the declared arity of the thing being applied, and the arity check that would close the gap has not been written. changing

Const generics, and the arithmetic they admit

type Grid of (T, const ROWS: Int, const COLS: Int):
    cells: Array of T

type Padded of (T, const N: Int):
    cells: Array of T
    grown: Padded of (T, N + 1)
    shrunk: Padded of (T, N - 1)
    tripled: Padded of (T, N * 3)
    doubled: Padded of (T, 2 * N)

Const generics are in the core because tensor shapes are built out of them. Tensor of (F32, (batch, 768)) carries 768 as a generic argument, and 768 is not a type. Retrofitting that later means reopening the parser, the resolver and every snapshot, so it is here in F0 even though tensors are not.

The grammar is five operators and no more: +, binary -, unary -, * and /, with * and / each requiring an integer literal on one side. That is the complete list, forever, and every addition to it is an addition to the normaliser, the equality procedure, the diagnostic renderer and the monomorphisation key. There is no %, no **, no max, no min, no comparison, no conditional, no function call, no const fn, no recursion and no escape hatch.

So the arithmetic is linear by grammar, not by a check run afterwards: N * M for two parameters is not a program the parser can build a node for, and it is reported there.

error[SC0157]: a const expression multiplies only by a literal
 --> grid.science:3:26
  |
3 |     bad: Padded of (T, N * N)
  |                          ^ one side of this needs an integer literal
  |
  = note: `const-expression-arithmetic.md` §2.1 keeps const arithmetic linear by grammar: two parameters may be added or subtracted, never multiplied or divided by each other

Division is specified and refused. The design gives N / 2 a quotient atom and an incomplete equality over it — N / 4 and (N / 2) / 2 denote the same function and no normal form proves it, so the compiler is meant to say cannot prove and print both. What the compiler does today is refuse the operator outright, which is the smaller and more honest state:

error[SC0260]: a const expression cannot divide yet
 --> grid.science:3:31
  |
3 |     halved: Padded of (T, N / 2)
  |                               ^ division in a const expression is F1
  |
  = note: `const-expression-arithmetic.md` §4 specifies the quotient atom; F0 is the quotient-free fragment, and multiplying by a literal is what F0 offers instead

A const parameter's annotation is a kind, not a type. Exactly two are admissible: Int, which is F0's, and Shape, a type-level list of Int expressions whose length is always statically known, which arrives with tensors. Bool is refused because a boolean that changes the rank of a return type is a type error waiting to be specified, and F64 because float equality is not equality — a normal form over floats is a normal form over a non-field with a non-value in it. The parser accepts anything in that position and lets the checker say so with a better message, which is the house pattern:

error[SC0220]: a const generic parameter's kind must be `Int` or `Shape`
 --> flags.science:1:30
  |
1 | type Flagged of (T, const F: Bool):
  |                              ^^^^ `Bool` is not a const-parameter kind
  |
  = note: `const N: K` annotates `N` with a kind, not with a type: `Int` is an integer known at compile time, and `Shape` is a type-level list of them

The normal form is a thing you can see

A const expression is normalised to k + Σ cᵢ·aᵢ: a constant, then coefficient-and-atom terms with the atoms in a total order stable across compilations. Equality is structural equality of that form, so A + B and B + A are the same type and a function may be declared with one and return the other. It is one linear merge over a sorted term list, with no fixed point and no possibility of non-termination, because no production in the grammar grows an expression.

type Buf of (const N: Int):
    x: Int

def same of (const A: Int, const B: Int)(p: Buf of (A + B)) -> Buf of (B + A):
    p

And when two forms are genuinely different, the diagnostic prints the normal form rather than the source, which is the part worth seeing: A + A comes back as 2*A, so a reader who wrote k + 1 on one side and 1 + k on the other can tell at a glance that the ordering is not the problem.

error[SC0525]: expected `Buf of 2*A`, found `Buf of A + B`
 --> buf.science:5:5
  |
5 |     p
  |     ^ this is `Buf of A + B`

Why refuse the general case at all? Because type equality on Grid of (T, ROWS, COLS) is const equality, and four separate things have to agree about it — type equality, shape equality, index bounds, and the key that decides whether two monomorphisations are the same function. Four implementations of "are these two extents the same?" is four answers, and the fourth one is a linker emitting two symbols for one function. A linear form normalises to a canonical k + Σ cᵢ·aᵢ; structural equality on that form is sound and complete, because the forms are the free ℤ-module on the parameters and evaluating at the basis vectors recovers the coefficients; and the normaliser never receives a non-linear input because the grammar admits none.

The cost is real and the design admits it. Rust's generic_const_exprs has been unstable since 2020, and it did not stall on normalising N + 1 against 1 + N — that part was understood early. It stalled on three things: its expression language is const fn, so equality of two const expressions is equality of two programs and no normal form can exist; it must prove a const expression well-formed before the parameter is known, which needs a predicate language and an entailment checker; and it may not report at instantiation, because separate compilation and dyn rest on the generic having been checked in the abstract. Science's answer to the first is the closed grammar above; to the second, refusal; and to the third, that it monomorphises everything anyway.

So Science pays for the refusal in post-monomorphisation errors: a library can ship a signature that breaks for your shape, and you meet the error inside code you did not write. The obligations are two rather than an open-ended set — a negative extent, and the solvability of const-argument inference — and the mitigation is that the diagnostic must name the instantiation, the parameter, the value and the call that produced it. If that chain is not rendered well, the decision is indefensible. The retreat is safe in one direction: const predicates in a where clause can be added later and every program that compiles today keeps compiling, because a predicate only rejects instantiations that would have failed anyway.

One amendment the implementation forced, and it is the kind worth recording: the normal form is the monomorphisation key, and the atom order is derived from a declaration's canonical path. The original claim — that the order is stable across runs without a hash — is false, and it is falsified by its own second clause: sciencec check a.science b.science and the same two files in the other order number their declarations differently. Within one compilation that changed no answer, because equality sorts both sides with the same function; what it changed was the serialised key, so the same program could produce different symbol names depending on how it was invoked — a cache miss rather than an error, which is the worst way to find out. The order comes from a canonical path and an index now, and the cost of the fix is that renaming a const parameter can reorder a normal form where renumbering a file no longer can.

T?, and the three things it is not

T? is a distinct type, not a union and not a subtype of T. T coerces into T? implicitly; T? never coerces to T. There is no Option, so there is nothing to construct — the present case is the value itself and the absent case is the literal null — and equally there is no map, no unwrap_or and no is_some, because there is no type left for those methods to hang off. The whole interface is the presence test ? and the narrowing it performs.

T?? is an error rather than a flattening. The parser builds two nullable nodes and the type checker collapses them, because a presence test on a presence test is never what anyone meant. The diagnostic is one of the better ones in the compiler and it explains the model in its note:

error[SC0520]: a type is nullable once
 --> opt.science:1:14
  |
1 | def f(x: Int??) -> Int:
  |          ---- already nullable here
  |              ^ this `?` adds nothing the first one did not
  |
  = note: `T?` is a distinct type holding a `T` or `null`, not a union, so there is no second absence for a second `?` to describe
  = help: the type is `T?`: delete `?`

What it costs in memory. A pointer-like T uses the null niche, so (borrowed T)? is one word. A T with no niche gets a discriminant byte, which is why an Int? occupies two words. An (any I)? is a nullable fat pointer with the niche in the data pointer, so it is two words and not three; the vtable pointer of a null interface object is undefined and never read. The two-word Int? is also the direct cause of the interpolation failure recorded in Strings and formatting: narrowing is a fact about the checker's view of a place and the layout is not narrowed with it.

Narrowing itself belongs to Errors, where the idiom lives, but one rule belongs here because it is a property of the type: narrowing is a fact about a place — a local, or a field projection from a narrowed place — and it is invalidated by any write to that place or to a prefix of it. config.port? narrows config.port and not config; writing to config invalidates it and writing to config.other does not.

Closures have a type, and it has no keyword

def apply(f: (Int) -> Bool, x: Int) -> Bool:
    f(x)

# `->` is right-associative, and `?` binds tighter than `->`,
# so a nullable closure needs its own parentheses.
type Pipeline:
    step: ((Int) -> Bool)?
    stages: Array of ((Int) -> Bool)
    curried: (Int) -> (Int) -> Bool

def twice(f: (Int) -> Int, x: Int) -> Int where Int: Eq:
    f(f(x))

(A) -> B reads as takes an A, gives a B. It is what Kotlin and Swift write exactly, what TypeScript writes with =>, and what the ML family writes with the arrow alone. The earlier spelling was function(A) returns B, which read as a noun naming what the parameter is; once returns became -> and function became def, the mechanical carry-over def(A) -> B was left naming nothing — a declaration that lost its name. The bare arrow sidesteps the problem by having no word to be the wrong part of speech, and it puts no new word on the reserved list. fn(A) -> B lost the audience test one to seven, and the one is PHP.

It parses on one token of lookahead and no backtracking: parse_paren_type reads (), (T) or (A, B) to completion, and then one peek decides — -> means that was a parameter list, anything else means it was a tuple. That is why a fallible return type -> (Config, Error?) stays a tuple: what follows it is : or where, never an arrow.

Three edge cases, all of which you will meet. It is right-associative, so (A) -> (B) -> C is (A) -> ((B) -> C), which is currying and the only useful reading. ? binds tighter than ->, so (A) -> B? is a closure returning a nullable and a nullable closure is ((A) -> B)?. And as a generic argument it needs its own parentheses — Array of ((Int) -> Bool) — for exactly the reason Map of (String, Int) does.

That last one does not fail; it means something else. Array of (Int) -> Bool parses cleanly, because the peek after (Int) finds an arrow and builds a closure type out of everything to its left. The field's type is (Array of Int) -> Bool: a closure that takes an array of integers. No diagnostic, no warning, and a type error somewhere downstream that names a type nobody wrote. It is the one silent misreading in the type grammar, and the only defence is the parentheses.

error[SC0525]: expected `Int`, found `(Array of Int) -> Bool`
 --> pipeline.science:5:5
  |
5 |     p.stages
  |     ^^^^^^^^ this is `(Array of Int) -> Bool

The one thing that cannot be spelled. (T) collapses to T with no node of its own, so a one-parameter closure whose single parameter is a tuple has no spelling: ((A, B)) -> C parses as a two-parameter closure. This is a genuine hole, and it is closed by a convention rather than by grammar — pairs in Science are records, so the only tuples in F0 are the return shape of a fallible function, and none of those is passed as an argument. If that stops being true, the answer is a named record and not a third paren.

Arrays and indexing#

[1, 2, 3] is a literal and a[i] is an index, with the bracket's role decided by parser position and nothing else. Indices are zero-based. m[i, j] is specified as a single index of arity two, and not m[i][j] — and it does not parse yet.

let primes be [2, 3, 5, 7, 11]
let identity be [[1.0, 0.0], [0.0, 1.0]]
let mutable counts be [0, 0, 0]

counts[1] be 9

print(f"{primes[0]} {identity[1][1]} {counts[1]}")
print(f"{primes.length()}")

That block checks and does not build. Arrays reach the back end as a value type it has no lowering for, and an index is a bounds check followed by an address computation of which neither half is emitted. Nothing in this section can be run yet, which is why nothing in it claims an output. changing

error[SC0525]: expected `String`, found `an integer literal`
 --> counts.science:1:33
  |
1 | let counts: Array of String be [1, 2, 3]
  |                                 ^ this is `an integer literal`

error[SC0525]: expected `String`, found `an integer literal`
 --> counts.science:1:36
  |
1 | let counts: Array of String be [1, 2, 3]
  |                                    ^ this is `an integer literal`

error[SC0281]: the elements of this array literal do not have one type
 --> mixed.science:1:15
  |
1 | let xs be [1, 2.0]
  |            - this is an integer literal
  |               ^^^ this is a floating-point literal
  |
  = note: an array literal is an `Array of T` where `T` is the unification of its elements (§3.1), and there is no implicit numeric conversion (§5.1): write the suffix, the `as`, or the literal you meant

error[SC0282]: this empty array literal has no element type
 --> empty.science:1:11
  |
1 | let xs be []
  |           ^^ nothing here says what `[]` holds
  |
  = note: an empty literal takes its element type from the expected type at its position (§3.3), and there is none here: annotate the binding — `let xs: Array of F64 be []`

let xs: Array of F64 be []          # the annotation supplies the element type
let ys be [1, 2, 3]                 # Array of I64, by defaulting
let zs: Array of F32 be [1.0f32, 2.0f32]

print(f"{ys[0]}")

The bracket, and the rule that decides which one it is

[ in prefix position opens a literal; [ in postfix position is an index. In a Pratt parser this is not so much a rule as a consequence — it is the null denotation against the left denotation, exactly as ( already means grouping in one position and a call in the other. No lookahead, no backtracking, no type information.

Whitespace is not load-bearing, so a [1] is an index exactly as a[1] is — forced by consistency with the decision not to make the space in Array of Doc .new() significant. A postfix bracket binds as tightly as a call and a field access and associates left, so a[i].field[j] groups as ((a[i]).field)[j]. A [ at the start of a line cannot attach to the previous line's expression, because outside brackets only a leading . or where continues a line; and inside brackets newlines are ignored, so the only reading available is the sensible one. JavaScript's equivalent hazard comes from automatic semicolon insertion, which Science does not have.

The earlier design spelled generic arguments Array[Doc], which would have made Name[ a choice between instantiation and index — a resolution question inside the parser, which is where languages with this problem end up needing a turbofish. of took that job and the bracket was freed for this one.

a[i][j] and a[i, j] are different programs and stay different. The first is two index operations, which is right for an Array of (Array of T). The second is one index operation of arity two, which is what a tensor or a matrix wants, and the comma inside the brackets is grammar rather than a tuple constructor: a[t] where t is a pair does not index a rank-2 thing. Aliasing the two was considered and refused — on a tensor, m[i][j] would have to synthesise a row view for every element access in an inner loop, and the reader could not see which they wrote.

The arity-two form is not in the grammar today. An index bracket holds exactly one index position, and a comma inside one is a parse error. The design asks that the parser and AST carry index arity from the first commit so that F1 adds a type rule rather than a syntax revision; that has not happened, so the revision is still owed. changing

error[SC0100]: expected `]`, found `,`
 --> matrix.science:2:9
  |
2 |     xs[1, 2]
  |         ^ expected `]`, found `,`

A literal is always an Array. Its type is Array of T for the unification of its element types, and it is never inference-directed into some other collection — a literal whose type depends on where you put it is a literal you cannot read locally. Other collections go through From over a chain: Set.from(["a", "b"].iterate_consuming()). That is more to type than a brace literal, and the cost is accepted: one literal form, one type, no set-versus-dict brace war. A matrix is a nested literal handed to Tensor.from, which checks the shape from the literal's syntactic shape — so there is no matrix literal form and no second bracket grammar to learn.

A trailing comma needs no new rule, because one is already allowed in every bracketed and parenthesised list and an array literal is a bracketed list.

Both of the rules in that paragraph are enforced: [1, 2.0] is SC0281 and [] with no expected type is SC0282. The callout above has both diagnostics and the reason the first of them was worth more than it looks.

Bounds, and the two ways of asking

Every a[i] raises an obligation — 0 ≤ i and i < extent(a) — which the compiler tries to discharge from a closed list of four rules, deliberately not a solver. Discharged means the compiled code contains no check and the expression cannot fail. Undischarged means a runtime check that panics — and a diagnostic, SC0286, saying so, a warning by default and an error under a verified profile.

Everything else is undischarged, and the named non-examples are a[compute(x)], a[i - 1], and a[i] where i came off a CSV. Rust and C++ make the same choice silently: you cannot tell by reading a[i] whether it compiled to a load or to a load with a branch, and you certainly cannot tell whether it can abort a six-hour run at hour five. The whole difference here is the diagnostic, and its message quality is the feature rather than a polish item — a message that only said "bounds check inserted" would be turned off within a week.

The fallback panics and it is not a type error, which is the honest half of the decision: making a[i] return a nullable would put a test on the hot path of every inner loop in the language, and the code that wants the test already has one. get is that spelling — def get(self, at: Int) -> (borrowed T)?, with the parentheses required because borrowed T? would read as borrowed (T?) — and it is what the genuinely dynamic case uses.

The last row is the one to push hardest: an index that could have been a chain is a code smell, and an index that is not written cannot be off by one.

None of the bounds machinery exists. There is no SC0286, no discharger and no inserted check; xs[7] on a three-element array passes check in silence. changing

Two bracket shapes are caught, both on the syntax tree before types, because neither fix needs one:

error[SC0151]: this index bracket has no index in it
 --> rows.science:2:12
  |
2 | let y be xs[]
  |            ^^ `[]` indexes nothing
  |
  = note: an index bracket holds one index position: `a[0]`, `a[i]`, or a range, `a[1..5]`

error[SC0154]: this range starts at 5 and ends at 1, so it holds nothing
 --> rows.science:2:13
  |
2 | let y be xs[5..1]
  |             ^^^^ the start is past the end
  |
  = note: no fix is offered because which of the two bounds is wrong is not something the compiler can know

Zero-based, and why that is not an aesthetic choice

Science is zero-based, ranges are half-open, and a[-1] is an error rather than the last element. The one-based column — Fortran, MATLAB, R, Julia, Mathematica, Lua — is not a list of bad languages; it is close to a list of the languages a computational physicist learned in, and Julia in particular is the closest thing Science has to a direct competitor.

The argument is not elegance and it is not familiarity: it is the zero-copy membrane. A NumPy array and a Science tensor over the same buffer are looking at the same bytes, and there is no marshalling step where an index could be adjusted — that absence is the feature. If the two languages disagreed about which element is [0] the disagreement would be silent, since both indices are in range; undetectable by the compiler, since the wrong index was computed in Python; undetectable in review, since both sides read correctly and only the composition is wrong; and numerically plausible — a spectrum shifted by one channel, a batch off by one row, a time series lagged by one sample.

There is a second, internal argument: every one-based language pairs one-based indexing with inclusive ranges, and Science's counting loop is 0..n, half-open, which was decided when ranges were. The cost lands on the computational-physics audience, who index from one in every paper they have ever read, and there is no cheap mitigation; offset-configurable arrays were considered and refused, because two conventions in one program is the failure the decision exists to prevent, and because they would make the index obligation above unprovable in general. It is also irreversible: no formatter rewrite turns one-based source into zero-based source, because the compiler cannot tell an intentional a[1] from a transcribed one.

error[SC0152]: a negative index does not count from the end in Science
 --> rows.science:2:16
  |
2 | let last be xs[-1]
  |                ^^ an index runs from `0` up to the extent
  |
  = note: Python reads `a[-1]` as the last element, which is what makes `a[i - 1]` in a loop read the last element at an `i` of zero instead of failing
  = help: read the last element with: `.last()`

Slices borrow

samples[1..5] has type Slice of T, which is { borrowed T, Int } — a pointer and a length — and it does not copy. Copying is not a close call: a column of a ten-gigabyte frame is pitched as the actual contiguous buffer, and a copying slice would mean taking half of it costs five gigabytes and a memcpy. The mutable form is MutableSlice of T and is produced through IndexMutably. The rank rule is NumPy's on purpose: an index position that is an integer drops its axis, and one that is a range or a bare .. keeps it. In F0 a slice is contiguous and one-dimensional over Array; strided and multidimensional views are F1, on Tensor, because a column of a row-major matrix is not contiguous and { ptr, len } cannot represent it.

Ownership needs no new rule for any of this. A slice is a borrow, so an array that has been sliced cannot be pushed to while the slice is live — push takes mutable self and the borrow rule forbids it — and "mutate while iterating" and "write through a view of the thing you are reading" are the same compile error. That is the NumPy aliasing bug, the one where a view of the array you are writing to produces a wrong answer with no error, removed by machinery that exists for unrelated reasons. It also costs something every NumPy user will hit once: let s be a[1..5] pins a for as long as s lives.

error[SC0538]: a range index would produce a slice, and there is no `Slice` type
 --> window.science:2:5
  |
2 |     xs[1..3]
  |     ^^^^^^^^ slicing a `Array of Int` is not implemented
  |
  = note: `a[1..5]` is specified as a `Slice of T` — a borrow and a length, which does not copy (§2.3) — and this compiler declares no such type. Index one element at a time, or iterate: `xs.iterate().skip(1).take(2)`

Closed ranges parse and are then refused by the type checker; open-ended ones do not parse at all. xs[1..3] reaches SC0538 above. xs[..2], xs[2..] and xs[..] are specified — the rule is that inside an index bracket a .. may omit either end, decided on one token of lookahead (after .., a ] or , means no end; before it, a [ or , means no start), and outside one both ends are required — and the parser reports SC0105. changing

error[SC0105]: expected an expression, found `..`
 --> rows.science:2:13
  |
2 | let y be xs[..2]
  |             ^^ expected an expression, found `..`

The reason open ends are confined to index brackets is that outside one, a .. with no right operand would have to be told from a .. that ends a line — which makes a line break load-bearing inside an expression. Inside a bracket the question cannot arise, because newlines and indentation are ignored entirely inside unclosed brackets. Storing a half-open range in a variable is the case that would be lost, and nobody has asked for it.

.. is looser than every operator, which is why a[0..n - 1] reads as 0..(n - 1) and not as a subtraction from a range. The precedence table does not place it; the parser does, and this is the sentence that records it.

Indexing is an interface, so your type can be indexed

type Row:
    label: String
    values: Array of F64

Row implements Index of Int:
    type Output is F64

    def index(self, at: Int) -> borrowed F64:
        self.values[at]

def first_value(row: borrowed Row) -> F64:
    row[0]

The two interfaces are Index of Idx, with def index(self, at: Idx) -> borrowed Self.Output, and IndexMutably of Idx, with def index_mutably(mutable self, at: Idx) -> mutable borrowed Self.Output. a[i] on the right of a be requires the first; a[i] be v requires the second. Both are declared in the prelude with their associated Output, which is a correction: a design note recorded, accurately at the time, that Doc implements Index of Int: could not be written at all, because the prelude's Index was a bare name with no parameter, no associated type and no method. It can now, and the listing above is the evidence.

A type with neither implementation is refused by name, and the note says where the fix goes rather than talking about mutability in the abstract:

error[SC0535]: `Doc` does not implement `IndexMutably`
 --> doc.science:5:5
  |
5 |     d[0] be 1
  |     ^^^^ `[]` needs `IndexMutably` and `Doc` has no implementation of it
  |
  = note: every operator is an interface method (§5.4): the block
         `Doc implements IndexMutably:` is what gives `Doc` this operator

IndexMutably is declared and is not yet writable, for a narrow reason: its body has to produce a mutable borrowed Self.Output, and indexing yields a shared borrow, so there is no expression in the language today that satisfies the signature. So the diagnostic above names a repair that cannot currently be carried out. changing

String implements neither, deliberately. A String is UTF-8, so there is no single right meaning for [0] — byte 0, character 0 and grapheme 0 are three different things — and the specified diagnostic, SC0258, names all three alternatives (line.bytes()[0], line.characters().first(), line.slice(0..n)) rather than refusing. It does not fire: line[0] on a String passes check today. changing

No comprehensions, and the reason is a formatter

error[SC0153]: Science has no comprehensions; write the chain
 --> rows.science:2:16
  |
2 | let doubled be [each * 2 for each in xs]
  |                ^^^^^^^^^^^^^^^^^^^^^^^^^ this bracket holds a comprehension, not a list
  |
  = note: the chain does the same thing, lazily and in reading order: `source.iterate().keep(<condition>).map(<expression>).collect()`
  = note: `keep` comes before `map`, and `each` names the element, so the chain declares no loop variable

The decision concedes the other side first. For the short case the comprehension is shorter — twelve tokens against nine — it is a single expression with no intermediate names, and it maps onto the set-builder notation this audience writes in papers. Anyone who says the chain is obviously better for it is selling something. What decides it is the rule one revision old: two spellings of one operation are permanently un-normalisable, because a formatter cannot canonicalise between them without running after type checking, and a formatter that must run after type checking is not a formatter. That argument deleted the word forms of every comparison. Adding comprehensions one section later would be incoherent.

Three supporting reasons, in descending weight: a comprehension is eager and the chain is lazy, so the beloved form would be the one that always allocates the intermediate; it does not scale past the short case, where nested for clauses read in an order nobody defends; and it reads backwards, with the operation before the source, which is why comprehensions do not compose with each other and chains compose trivially. SC0153 is detected on the syntax tree, before types, because a comprehension does not type-check as anything and catching it later would produce a cascade. If it ever comes back, it must come back as pure sugar that desugars to the chain and introduces no semantics of its own.

Functions#

def declares every function form there is. Generic parameters follow the name with of; bounds go inline or in a where clause, and several join with +.

interface Summarize:
    def summarize(self) -> String
    def preview(self) -> String:
        self.summarize()

type Doc:
    title: String
    body: String

type Pair of (A, B):
    first: A
    second: B

def summary_length(doc: borrowed Doc) -> Int:
    doc.body.length()

def duplicate of T: Clone + Eq(value: borrowed T) -> Pair of (T, T):
    Pair(first: value.clone(), second: value.clone())

def longer_of of T(left: borrowed T, right: borrowed T) -> String
        where T: Summarize + Clone:
    if left.summarize().length() >= right.summarize().length():
        left.preview()
    else:
        right.preview()

def paired of (A, B)(first: A, second: B) -> (A, B):
    (first, second)

Generic functions check and do not build. Nothing monomorphises them: the walk that would turn duplicate of T into one emitted function per concrete T sits above the back end and no phase runs it, so a call to one is SC0400. Tuples are refused for a different reason — there is simply no arm mapping a tuple type to a layout. changing

The last expression of a body is its value. return exists for leaving early and is not written at the end of a function. This is the ML and Rust convention rather than Python's, and it is one place the language expects a Python reader to look twice: there is no implicit None. A function with no return type returns () — and the rule is stricter than "the value is discarded": the last expression must be (), so a trailing x of type Int in a function declared without a return type is a type error, not a thrown-away value.

error[SC0525]: expected `()`, found `Int`
 --> unit.science:2:5
  |
2 |     x
  |     ^ this is `Int`

How a body is checked

Signatures are fully annotated; bodies are fully inferred. Checking is bidirectional and there is no unifier across function boundaries: every call site knows its callee's types before it looks at the arguments, and every body has a known expected return type, which gives a checking mode where the type is known and a synthesis mode where it is not. There is no Hindley–Milner, no generalisation, no let-polymorphism and no principal types. Global inference was rejected on two grounds: it does not hold up in the presence of interfaces and regions, and its errors point far from the fault — which, for a language whose diagnostics are the only teaching channel it has, is disqualifying.

Three things follow, in the order the design ranks them. Every diagnostic can point at an annotation a human typed. Bodies check in parallel and in any order, which is what makes the incremental boundary a function rather than a component — the memoised unit is one body, keyed on its hash plus the signatures it references, so editing a body invalidates that body and editing a signature invalidates every body that calls it. And it is expressible in Science, which matters because the compiler intends to compile itself: a bidirectional checker is a recursive walk with an environment, where a unification-based one wants a mutable union-find with interior mutability, which the language has no spelling for.

Local inference variables still exist, because let xs be (Array of Int).new() has to get its element type from a later push. So there is a small unification engine inside one body; it is bounded by the body and discarded when the body is done. Numeric literals go through it: an unsuffixed literal is inferred and only defaulted to I64 or F64 when nothing constrains it, because a language that silently makes 1 an I32 will be wrong on somebody's index arithmetic.

The auto-borrow is not in the type relation, and the measurement that forced the distinction is worth quoting. A parameter declared borrowed T is called with a T: the caller does not write the borrow and the checker inserts it. That is an elaboration, not a coercion — the value is unchanged and what the checker writes down is a Borrow node the author did not — so it lives in the body checker rather than in assignability, whose own table knows nothing about regions. The first run of the finished checker over the corpus produced 147 diagnostics, roughly 60% of which were a borrow the language had told the author not to write. Its cost is two places where the checker's tree no longer matches the token stream one to one, which MIR pays rather than the reader.

The practical consequence of all this is that you write types at a boundary and nowhere inside one. It is also why tools --json can derive a schema before anything is run: the parameter types are already written down.

What a call may not do

There are no default arguments, no named arguments and no variadics. Each absence is load-bearing somewhere else on this page: no variadics is the decisive reason print is unary; no defaults is why BufferedReader.new(source, capacity) takes its capacity explicitly; and named arguments exist in the grammar but belong to record construction, so using them on a function says so.

error[SC0527]: this call takes 1 argument and was given 2
 --> call.science:4:10
  |
4 | let y be f(1, 2)
  |          ^^^^^^^ 2 given

error[SC0201]: the name `f` is defined more than once
 --> call.science:4:5
  |
1 | def f(x: Int) -> Int:
  |     - first defined here
...
4 | def f(x: Int) -> Int:
  |     ^ defined again here

No overloading is the reason method resolution can pick a callee before inference runs. A method's argument labels are part of its name — sorted() and sorted(by: key) are two names, not one name with two signatures — and the rule for when to use a label is that the verb either already names its argument (take(5), map(f), keep(p)) or it is selecting between variants of one verb, in which case it takes one.

Closures: two forms, and nothing else

each names the subject and declares no binder; x giving … declares one. They differ in a real property, which is why there are two: each cannot nest, and the compiler can tell them apart for exactly that reason. The canonical form — what a formatter would produce — is each when the parameter occurs once and the closure is not nested inside another closure's argument, and giving otherwise.

def shortlist(xs: Array of Int) -> Int:
    xs.keep(each > 5)                       # implicit subject, mentioned once
    xs.keep(x giving x > 5 and x < 50)      # named, because it is mentioned twice
    0

error[SC0115]: a nested `each` would name a different subject than the `each` around it
 --> nest.science:2:21
  |
2 |     xs.map(each.map(each + 1))
  |                     ^^^^ this `each` is inside another `each`
  |
  = note: name the parameter instead, with the `giving` form: `outer.map(item giving item.inner.map(each.x))`

There is no lambda, and the refusal has four independent reasons. It is not a mechanism — lambda x: x > 5 and x giving x > 5 differ in no property at all, produce the same node and the same dump. It would be a third spelling, and the longest one. The formatter argument is sufficient on its own: with no syntactic property to distinguish them, either lambda is canonical somewhere, by an arbitrary rule that will drift, or it is canonical nowhere and sciencec fmt deletes every occurrence on its first run. And decisively, λ is a primary named quantity in five fields — wavelength, decay constant, eigenvalue, Poisson rate, ridge strength — always in binding or parameter position, where no positional rule can rescue it. let lambda be 532<nm> must stay a legal line.

The migration diagnostic for it is specified and does not fire. SC0135 is meant to recognise the shape — an identifier spelled lambda followed by :, or by a name and :, or by a name and -> — and offer the giving rewrite as an applicable fix, while leaving lambda a free identifier everywhere else. What a reader gets today is a bare parse error, twice:

error[SC0100]: expected `)`, found `x`
 --> filter.science:2:20
  |
2 |     xs.keep(lambda x: x > 5)
  |                    ^ expected `)`, found `x`

error[SC0100]: expected end of line, found `x`
 --> filter.science:2:20
  |
2 |     xs.keep(lambda x: x > 5)
  |                    ^ expected end of line, found `x`

A closure takes one parameter or none. There is no two-parameter form. The AST node carries an Option of one binder, and the proposed extension — (acc, x) giving acc + x — is not decided, because it belongs to whoever ships fold. (a, b) giving … does not parse. changing

That absence is protecting against something specific, and it is worth knowing even though the form does not exist. The parser tests for a named argument by looking for an identifier then a colon, and it splits arguments on the top-level comma first. So a two-parameter closure written with a comma would have its second half, b: a + b, satisfy the named-argument test exactly, and the call would parse — silently — as two arguments. SC0137 is allocated for it.

What is not written down anywhere is how a closure captures. The design says the two forms "capture the same way" and never says what that way is — there is no by-borrow-versus-by-move rule, no move analogue, no closure-value type, no statement about storing one in a field, and no Fn-style hierarchy, neither adopted nor rejected. Every attested use is an immediate argument to a chain method. One consequence is fixed in advance for a reason unrelated to ergonomics: a closure must be typed by its captures rather than erased, from F0, because a future .parallel() has to reject a closure that captures something mutable borrowed, and nothing in F0 reads that information — which makes it the requirement most likely to be quietly missed.

error[SC0156]: the declaration is written `def`
 --> old.science:1:1
  |
1 | function old_style(x: Int) -> Int:
  | ^^^^^^^^ `function` is not a keyword in Science
  |
  = note: `def` declares every function, method and interface member
  = help: write the declaration as: `def`

That fix is machine-applicable, which is the property that matters most here. Science has no training corpus and will not have one for years, so for a model writing Science the diagnostics are not the fallback channel — they are the only channel. A loop that can apply a fix converges in one round trip; a loop that must infer the fix from prose sometimes does not converge at all. The same reasoning is why one mistake must cost one message: a human fixes the first of three cascaded errors, and a model attempts three fixes, two of which are wrong.

SC0156 meets that bar in a way the lambda and += cases above do not, and the mechanism is recovery rather than recognition: the parser consumes the stale keyword and continues as though def had been written, so the parameters, the arrow and the block are all checked normally and the file produces one error instead of three. The recognition costs one token of lookahead and buys back the identifier function, which a C binding somewhere needs as a struct field name. That is the trade the dot rule proposes to make everywhere: a position test instead of a reservation.

Interfaces#

An interface is a set of requirements a type can satisfy. It may carry required methods, default bodies that call them, and associated types. Implementations are statically resolved.

type Doc:
    title: String
    body: String

type Position:
    line: U32
    column: U32

interface Summarize:
    def summarize(self) -> String

    # A default body may call any other method of the interface,
    # including one it does not itself provide.
    def preview(self) -> String:
        self.summarize()

Doc implements Summarize:
    def summarize(self) -> String:
        self.body.replace("\n", " ")

Position implements Copy            # a marker: one line, no block

Doc implements Summarize reads in the order the sentence goes, which is the reverse of Rust's impl Summarize for Doc. A marker interface — one with no methods — is implemented on one line, because F0 has no empty block and inventing one for this case would be a grammar rule bought for a formatting preference. Interfaces are named as verbs for what an implementor does — Iterate, Display, Inspect, Summarize — and the method is the same word in lower case, which keeps write the free function and Write.write the method in different namespaces.

The orphan rule applies, and it is one of the few rules in this section the compiler enforces. An implementation is legal only if the interface or the type belongs to the module declaring it. Without it, two libraries can each implement one interface for one type, both compile, and the program that uses both has two answers to one question with no way to say which it wanted — decided by the linker. This is a package-level rule and the package manager does not know about it yet.

error[SC0207]: this implementation is an orphan: neither the interface nor the type belongs to this module
 --> shim.science:1:1
  |
1 | String implements Display:
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^ declared here (continues to line 3)
  |
  = note: the interface `Display` belongs to `core`
  = note: the type `String` belongs to `core`
  = note: wrap the type in a record of your own and implement the interface for that
  = note: the prelude is a module no file can name, so there is nowhere to move this implementation to

The last note is the one that makes the rule bite rather than merely inconvenience: for a prelude type and a prelude interface there is no module you could move the implementation to, so the remedy is a wrapper record and not a relocation. Either half being local is enough — your type with a prelude interface, or a prelude type with your interface, both compile.

type Doc:
    title: String

interface Summarize:
    def summarize(self) -> String

Doc implements Summarize:
    def summarize(self) -> Int:     # the interface says String
        0

    def extra(self) -> String:      # the interface never declared this
        self.title

Doc implements Summarize:           # and again, for the same type
    def summarize(self) -> String:
        self.title

error[SC0534]: `Doc` does not implement `Summarize`
  --> show.science:11:5
   |
 7 | def show of T(x: borrowed T) -> String where T: Summarize:
   |                                                 --------- `T` was declared `Summarize`
...
11 |     show(d)
   |     ^^^^^^^ `T` is `Doc` here
   |
   = note: an implementation is a block the program writes: `Doc implements Summarize:`

Receivers, and what each one costs

type Doc:
    title: String
    body: String

Doc has:
    def summarize(self) -> borrowed String: # shared borrow of the receiver
        self.body.trim()

    def reset(mutable self):                # exclusive borrow
        self.body be String.new()

    def into_title(self: Self) -> String:   # consumes it
        self.title

    def new(title: String) -> Doc:          # no `self`: an associated function
        Doc(title: title, body: String.new())

let doc be Doc.new("inferred, never written")
print(doc.summarize())

The three receiver forms are the three things a method can do to the value it is called on, and they are not interchangeable. self: Self is what makes a builder's final build() or a handle's close() impossible to call twice. Note that self is already the shared borrow — there is no borrowed self, and writing one is a parse error, because the bare receiver is the borrowing one and a second spelling would mean nothing new. That fact is also where the interpolation guarantee comes from: Display's method takes self, so rendering a value cannot consume it.

None of the three is enforced yet. Calling a mutable self method through a shared borrow checks clean, for the same reason assigning to an immutable binding does: the mutability half of the borrow rules is not wired in. changing

A function with no self is an associated function, called through the type: Doc.new(…). It is how Science spells a constructor, and there is no special constructor syntax because a constructor is a function that returns the type, which the language can already say. Variant construction uses the same dotted spelling, so IoError.NotFound(path) and Doc.new(title) read alike deliberately.

Method calls check and do not build. The resolver finds the method and the checker types it, and then the tree does not record which function was found, so the receiver arrives at the back end as an unresolved Self. Every listing in this section therefore stops at check. changing

Method lookup

Lookup is the inherent methods on the type, then the interface methods from interfaces the type implements that are in scope. Ambiguity is an error, never a priority ordering — a language that resolves a collision by preferring one source teaches a rule nobody can see at the call site. Both failures name what was searched:

error[SC0532]: `borrowed Doc` has no method `no_such_method`
 --> doc.science:5:7
  |
5 |     d.no_such_method()
  |       ^^^^^^^^^^^^^^ no such method
  |
  = note: method lookup finds the inherent methods of the type and the methods of the interfaces it implements, and neither has this name

error[SC0528]: `borrowed Doc` has no field `no_such_field`
 --> doc.science:5:7
  |
5 |     d.no_such_field
  |       ^^^^^^^^^^^^^ no such field

Both messages print the receiver as borrowed Doc rather than Doc, which is accurate and is the auto-borrow becoming visible: the parameter was declared borrowed Doc and the lookup happens on that type. It is a small thing and it is the kind of small thing that makes a reader think the borrow is the problem when it is not.

Associated types

interface Iterate:
    type Item
    def next(mutable self) -> Self.Item?

type Countdown:
    remaining: Int

Countdown implements Iterate:
    type Item is Int

    def next(mutable self) -> Self.Item?:
        if self.remaining <= 0:
            null
        else:
            self.remaining be self.remaining - 1
            self.remaining

Associated types are in F0 because without them Iterate cannot name its element type and no generic container interface can be written at all. An associated type belongs to the implementation rather than to the interface: a Countdown yields Ints and there is no second way to iterate a Countdown, which is exactly the difference between an associated type and a generic parameter. It is declared type Item in the interface and type Item is Int in the implementation, projected as Self.Item with a dot, and constrained in a where clause with is: where Self.Item is borrowed T, T: Clone.

An exhausted iterator returns null. Self.Item? is the nullable type; there is no wrapper to construct, so the present case is the value itself and the absent case is the literal. That is smaller than an Option, and it is also less: there is no map, no unwrap_or and no is_some, because there is no type left for those methods to hang off.

Iterate is also the shape of the whole chain API: one required method, next, and thirty-eight provided ones beside it. Users implement a source and never a combinator, which is what lets a future parallel form hand the identical vocabulary to a different trait without touching user code. The one other member, estimated_length, is defaulted so that implementing a source stays a one-method job, and it exists now rather than later because collect() preallocates from it.

Operators are interfaces

type Vector2:
    x: F64
    y: F64

Vector2 implements Add:
    def add(self, other: Vector2) -> Vector2:
        Vector2(x: self.x + other.x, y: self.y + other.y)

Vector2 implements Eq:
    def eq(self, other: borrowed Vector2) -> Bool:
        self.x is other.x and self.y is other.y

let sum be Vector2(x: 1.0, y: 2.0) + Vector2(x: 3.0, y: 4.0)
print(f"{sum.x is 4.0}")

The full list is Add Sub Mul Div Rem Pow MatMul Neg Index IndexMutably Eq Ord Copy Clone Drop Iterate From Display, and Error beside them. A scientific language in which + does not work on your own type is not a scientific language, so implementing an operator interface is how a user type joins in. Eq and Ord are what the comparisons dispatch to, and because there is exactly one spelling per comparison there is no second form for a parser rule to drift from.

Of those nineteen, four are declared with a method. Error has message, Iterate has next and its Item, Index and IndexMutably have theirs. The other fifteen — Add, Eq, Ord, Copy, Clone, Display and the rest — are names the prelude declares with no methods on them at all. So there is no .clone() to fall back on and no Display.display to call through, which is the same fact that keeps print's argument type undeclared. Writing Vector2 implements Add: with a body works, because a block's method set is open; what does not exist is a declared shape for the compiler to check it against. changing

Operators on primitives do not go through an implementation either, and the mechanism is not what it looks like. A design amendment said the operator interfaces are implemented for borrowed operands of the primitives; asking the compiler, they are not. What happens is that a borrow of a Copy type coerces to a value at each operand, so the checker sees F32 + F32 and never asks about a borrowed implementation. That is better than the amendment, because it is one rule rather than a table of ten operators over a dozen numeric types — and it is also narrower, because it does not reach a non-Copy type: borrowed String + borrowed String does not work, where the amendment as written implies it would.

Copy and Clone are the two that will catch you. Copy means assignment duplicates instead of moving, and it is for small values whose duplication is a register move. Clone means duplication is explicit and possibly expensive. Every numeric type, Bool and Char are Copy; String deliberately is not, because an owned copy of a String allocates and calling that a copy would hide the allocation. A type that is neither — which is most types — moves when you assign it, and that is the subject of the next section.

Interface objects, and what dispatch costs

any I is the interface object: one function in the binary rather than one per type. There are four spellings and they cost different things. borrowed any I is a pointer paired with a vtable known at the site and emits no code at all — it is unsizing, and it is implicit. any I and Box of any I own the value, which means it moves to the heap, which allocates, and those two are written out rather than inserted. And (any I)? is a nullable fat pointer whose niche lives in the data pointer, so it is two words and not three.

That is the line the implicit-conversion set is drawn on, and it is worth stating because counting the variants gives a different answer than the design does. The rule is no implicit change of a value, not no implicit conversions — boxing preserves the value where the From widening that was deleted did not. By that measure there are two implicit conversions that change a value, and the implementation carries seven coercion variants: T into T?; a concrete error into any Error at a return and at an argument; borrowed C into borrowed any I for any interface; and borrowed T into T when T: Copy, in three shapes. A reader counting variants and concluding the note is stale is reading the right number and the wrong question.

One rule keeps interface objects usable at all: a method whose signature mentions Self by value is automatically excluded from the vtable, with no user-written bound to say so, and calling it on an any I value is SC0271. That is what lets any Iterate exist despite the combinators all consuming self.

The Copy rule that lets a borrow be read as a value

A shared borrow of a Copy type is assignable to the type itself. borrowed Int where an Int is wanted reads the value out, because the whole content of Copy is that a copy of the value is the value: no allocation, no drop, no observable second thing. Three conditions, each refusing something different — the borrow must be shared, so that mutable borrowed T does not become usable wherever T is; the referent must be exactly the target, so the rule takes one borrow off and composes with nothing else; and the referent must actually declare Copy, which a bare T: Copy bound on a type parameter does not.

It is in the language because the alternative was an expressive dead end. Science has no dereference operator, by design, and Array.get returns (borrowed T)? — so before this rule there was no spelling that read a Char out of a container. It is also what makes the most-written loop in the language legal: Array of T iterates at borrowed T, so for n in numbers: binds n as a borrow and every arithmetic operator in every loop body meets one. Without the rule, total be total + n is a type error.

The design is candid that this is a weaker rule than the other implicit conversions in the language: unsizing a borrow into an interface object emits no code at all, and this one emits a copy, so "the same value" is doing work that "no work happens" did before. It earns the weaker defence by the dead end, not by convenience — and the back end refuses it today, so the loop it exists to permit type-checks and does not yet build. changing

Ownership and borrows#

Memory is managed at compile time. Every value has exactly one owner; assigning, passing or returning moves that ownership unless the type is Copy; leaving scope destroys the value. There is no garbage collector, no reference counting, and no lifetime annotations to write.

type Doc:
    title: String
    body: String

type View:
    source: borrowed Doc           # a record may hold a borrow; the region is inferred

def retitle(doc: mutable borrowed Doc, title: String):
    doc.title be title

def compare(left: borrowed Doc, right: borrowed Doc) -> Bool:
    left.title is right.title

let mutable doc be Doc(title: "a", body: "")

# A parameter declared `borrowed` is borrowed automatically, so the call
# site is bare. The signature still carries the information.
retitle(doc, "renamed")
print(f"{compare(doc, doc)}")

# Write the borrow out where the position is not a call site.
let view be View(source: borrowed doc)
print(view.source.title)

The rules, in full, are six lines. Every value has one owner. Assigning, passing or returning moves it unless the type is Copy. Using a moved value is SC0301. A value may be borrowed shared any number of times, or exclusively once, never both at once. No borrow outlives its referent. Leaving scope destroys the value, running Drop if it has one. Everything else in this section is a consequence of those six.

Move, and the four shapes a move is not reported in

error[SC0301]: use of a moved value
 --> twice.science:9:10
  |
8 | let a be take(d)
  |          ------- `d` is moved here
9 | let b be take(d)
  |          ^^^^^^^ ...and moved again here, after the move
  |
  = note: every value has one owner, and assigning, passing or returning it transfers that owner (§6.1 rules 1 and 2), so the name is empty afterwards (rule 3)
  = note: borrow at the earlier use instead of moving, or give the second use a value of its own; a type that is not `Copy` is never copied implicitly

Rule three is enforced, and the rule it is enforced by is stated in one sentence: one SC0301 per local, at the first point in the body where that local's state is gone, the move that put it there can be named, that move was of the whole local, and the local's type owns something. Each of those four conditions is a refusal to guess, and each of them lets a real mistake through. They are worth knowing individually, because they are the difference between a check you can rely on and a check you can only be surprised by.

Two more, from further upstream. A move through a call whose signature the lowering cannot see is invisible, because every argument of such a call is lowered as a copy — deliberately, since calling a move a copy hides an error and calling a copy a move costs at worst one unnecessary drop flag. And a move out of a closure capture is modelled as an exclusive borrow, so it is invisible too. Both are the same trade in the same direction: this check loses errors rather than inventing them, and every line above says which ones.

What a move leaves behind is nothing, and taking the name back is legal. After take(d), d names no value; writing d be Doc(title: "b") gives it one again, and every use after that is fine. A write to the whole local is not a use, it is a new value — which is the rule that makes the reassignment work. A write to a projection, d.title be "x", is a use, because it needs the rest of d to still be there.

SC0302 is allocated and reported from nowhere, and that is a decision rather than a gap. The note that reserved it described it as conflicting borrows, which is rule 4, which is already SC0330; emitting both would be two codes for one violation. What it is still owed is a specialisation for an extern declaration, and F0 has no such declaration to read.

Borrow: two kinds, and every position each may stand in

The spelling is exactly mutable borrowed, in that order, and mutable in a type never means anything else. There is no third kind of borrow and no unique/owned qualifier. Two English words where Rust has & and &mut is the whole of the trade: it is longer to type and it is the thing a reader who has never seen the language can still read.

mutable on a binding is a different word doing a different job. let mutable x be 0 says the name may be assigned again; mutable borrowed T says the borrow may write through. They share a keyword and nothing else, and the one place they meet is that taking a mutable borrowed of a binding requires the binding to be mutable. The language specifies that requirement; the diagnostic for it is SC0304, x is not mutable, whose suggested fix is written four ways — declare it let mutable x, bind it mutable x in the pattern, take the receiver as mutable self, or, for a parameter, bind a local, because a parameter cannot be declared mutable. changing

Auto-borrow at call sites, and the one rule it obeys

If a parameter is declared borrowed T, the caller writes compare(a, b) and not compare(borrowed a, borrowed b). The signature still says borrowed, so a reader keeps the information; only the noise at the call site goes. Rust rejected this and Mojo adopted it, and for this audience Mojo is right — a scientist reading gemm(&a, &b, &mut c) is reading three sigils that tell them nothing they could not have read in the signature.

It applies at an argument and nowhere else. let x: borrowed String be s is not a call site, so no borrow is inserted there and the word has to be written; admitting it would be a language change made by a type checker. What the checker does is exactly what the author was allowed to leave out — it writes down an ordinary borrow node — so the mid-level IR sees the same tree whether or not you typed the word, and the region engine gets a program point for the borrow either way. An explicit borrow stays legal where it clarifies, and it is required where the position is not a call site, as in the View construction above.

And it stops at a branch. In show(if flag: "yes" else: "no") the call site is the argument, not the two arms, so a borrowed String expectation is not pushed inward. Pushing it in made each arm borrow its own temporary, whose storage ends inside the arm, and the region checker then reported SC0333 on a correct program — right about the MIR, wrong about the program. Three of the four branching forms are treated that way.

The rule was almost lost, and how it was found is the argument for it. The design note that owns type checking never mentioned auto-borrow; the core spec requires it; and the implementation followed the note. The first run of the finished checker over the example corpus produced 147 diagnostics, roughly 60% of which were a borrow the language had told the author not to write. A rule the spec states and the design note forgets is worse than one neither has, because the implementation follows the note.

It also concealed a real bug for a while, which is the honest other half. Auto-borrow fired for borrowed any Summarize and not for borrowed T where T was generic, so describe(doc) silently moved doc; the corpus's largest example then moved a value that another value was still borrowing and used it twice more. The region engine found it, the type checker was fixed, and a test now stands on the program. A convenience that inserts something invisible is a convenience that can fail to insert it invisibly.

Two-phase borrows, so that b.push(b.size()) compiles

type Buffer:
    total: Int

Buffer has:
    def size(self) -> Int:
        self.total

    def push(mutable self, value: Int):
        self.total be self.total + value

def grow(buffer: mutable borrowed Buffer):
    # The exclusive borrow of `buffer` is RESERVED here and ACTIVATED after
    # the argument has been evaluated, so the shared borrow inside the
    # argument does not overlap it.
    buffer.push(buffer.size())

An exclusive borrow taken in argument position is two-phase; every other exclusive borrow is single-phase. A borrow bound to a name — let r be mutable borrowed x — is used an unknown number of times, and two-phasing that would be unsound. The distinction is carried all the way down: the mid-level IR has a reserve borrow kind and an explicit activate statement emitted immediately before the call, and the region engine treats a reserved borrow as not-yet-exclusive for the window between them.

The window is a reachability question, not an interval. It is the set of program points reachable from the reservation that can also reach the activation, with the activation itself outside it — computed in both directions rather than as every point between them in the numbering, because an argument list can contain an if and the numbering is not a path. This is the sort of detail that is invisible when it is right and produces an error on a correct program when it is wrong.

What the design notes did not settle. Neither note says what a reservation may coexist with, and in particular whether it must be compatible with a pre-existing shared borrow that ends before the activation. That makes rule 4 a three-state question — shared, reserved, exclusive — where it was written as a two-state one, and the implementation answered it by splitting the access: the reservation is not an exclusive access and the activation is. That split is what makes let s be borrowed v followed by v.push(s.length()) compile.

A borrow ends at its last use, and captures are borrows

def apply(f: (Int) -> Int, n: Int) -> Int:
    f(n)

let offset be 3
# `offset` is captured by borrow, and the borrow lasts as long as the
# closure value does — not to the end of the block.
print(f"{apply(x giving x + offset, 2)}")

That listing has no output under it because it does not build. A closure's captures are analysed, lowered and region-checked; its body is not lowered at all, because the resolver does not mint a definition for the closure itself, so there is nothing for the back end to emit. Everything this section says about captures is checked on every sciencec check; none of it runs. changing

Every capture is a borrow of the captured place, taken where the closure value is created and held for as long as that value is live — shared, unless the body writes through the place, in which case exclusive. There is no by-value capture and no copy capture, not even for a Copy type, and there is no move keyword to ask for one: move is reserved for a later phase and writing it today is a parse error.

The argument for one uniform rule is that no F0 program can tell the difference. Copy-capturing an Int and borrow-capturing it differ observably — the closure sees the old value or the new one — but under a uniform borrow capture the program that would notice does not compile, because the write to the captured binding conflicts with the closure's live shared borrow under rule 4. So the language has not yet had to decide, and it has not decided. Rust's three-way Fn/FnMut/FnOnce split is not available here anyway, because a closure's type is a bare arrow with no trait behind it.

Captures are keyed on the binding, never on a projection out of it. A body that names config.port captures config. That is coarser than Rust's per-field capture and it is deliberately matched to the move analysis, which tracks whole locals too — two passes that disagree about granularity produce answers that cannot be compared.

Drops, and the three things that can happen at one

Leaving a scope drops what the scope holds, in reverse order of creation. A return leaves every scope, a break leaves every scope down to the loop's, a continue the same. That is the entire timing rule, and it is the one thing ownership buys that a garbage collector cannot: the point at which a device buffer is freed is a point the compiler can name.

A conditionally moved local gets a drop flag — one byte, set where the value is initialised, cleared where it is moved, tested at the drop. The elaboration runs during MIR construction, before region inference, and it has exactly three outcomes: a local that is definitely live at the drop keeps the drop and gets no flag; one that is definitely gone has the drop deleted outright; and only the maybe case pays a byte and a branch. The largest program in the corpus produces zero drop flags, because it contains no conditional move — which is the measurement that says the flag is a fallback rather than a tax.

Drop is a name in the prelude and not yet a mechanism. It is declared as an interface with no method in it, because the note that would give drop a signature has not been written; a type may be declared to implement it and nothing reads the declaration. The back end is where this becomes visible: a drop of a String emits one call to free it, a drop of something that owns nothing emits a jump, and anything else — a flagged drop, or a drop of a value whose release would need generated glue — is SC0400, refused loudly rather than skipped, because skipping a drop-flag update is a double free. changing

What a region is, and why you never write one

A region is the set of program points at which a borrow is live — literally a set of (block, statement) pairs, held as a bitset, ordered by inclusion. That is a control-flow property, not a lexical one: a borrow ends at its last use, not at the closing of a block. The compiler assigns a fresh region variable to every borrow and to every reference inside a type, collects outlives constraints from assignments, calls and returns, propagates them to a fixed point, and then checks for conflicts. It does this over a control-flow graph, which is why the compiler has a mid-level IR at all.

The propagation has one shape and it is worth seeing. For a constraint 'a outlives 'b at point p, walk forward from p's successors; at each point, stop if 'b does not reach it, otherwise add it to 'a and carry on. Three lower bounds seed the whole thing: a local's region holds every point the local is live, a parameter's region holds every point at all, and a loan's region starts empty and grows only through the constraints. There is no upper bound anywhere in the solver, and that single fact is why one of the diagnostics below has never fired.

There are no elision rules, because elision is not the mechanism. Rust's lifetime elision is a convenience over a syntax that remains available when the guess is wrong; Science has no syntax to fall back on, so a function's parameter and return regions are simply an analysis result. Functions are analysed in reverse topological order of the call graph — Tarjan's algorithm, iterative — and mutual recursion is resolved by a fixed point over each strongly connected component, every member starting from the empty summary. Starting from the opaque one would also terminate and would conclude that every recursive function returns a borrow of everything, which is sound and useless.

A type gets one region variable per borrowed field, and the relation between them is inferred at each use site rather than declared once. Where Rust writes FftwPlan<'a> and puts 'a on both fields — asserting the two outlive the same thing — Science asserts nothing, and each construction generates its own constraints. That keeps information Rust's single name discards. It costs two things: a type's region stops being a property of the type and becomes a property of each value, and the intersection of two field regions can be empty, which means a value that is dead at birth and needs its own diagnostic rather than a generic conflict. That diagnostic, SC0335, exists and has never fired; the crate's own argument is that with no upper bound in the solver it cannot, and it is kept because the argument is about the shape of the solver rather than about programs.

What happens when inference has no single answer. Rust reports an error and makes you write 'a. Science cannot make you write anything, so it refuses the program: SC0340, with the offered fix being to return an owned value or an index instead. That is uncomfortable — it rejects a program for being ambiguous rather than wrong — and it is the honest consequence of removing the syntax. In the implementation it turned out narrower than specified: a return constrained by two parameters is not ambiguous, because the answer is a set and the caller intersects it, so what is left is a body that returns a reference and does not say where it points. If SC0340 fires often in real code, the no-syntax decision is wrong, and the design says so rather than assuming otherwise.

One thing the claim does not say, and should not be read as saying. Region inference is interprocedural within a crate. Across a crate boundary the inferred relation — for each return region, which parameter regions constrain it — would be serialised into crate metadata, because otherwise a module could not be checked without its dependencies' bodies. That summary carries exactly the same information a lifetime annotation does. It is computed today and it is not written anywhere, because there is no crate metadata format to write it into; a call to a function in another crate is answered with assume the worst. The claim is that a programmer never writes a region. It was never that the compiler does not need one. changing

What a borrow error looks like

With no 'a to print, a message has no choice but to describe the program, and that is a constraint worth accepting on purpose: the error is forced to be a narrative because it cannot be algebra. Three spans — where the borrow was born, what keeps it alive, where the conflict is. The "still needed here" span is the load-bearing one, and it is the one a solver that merged its constraints for speed can never produce, which is why provenance on every constraint was a decision taken before the solver was written rather than after. The constraint set is deliberately not deduplicated: the four lines that would shrink it would also delete the answer to why is this borrow still alive at line 90.

error[SC0330]: `doc.body` is borrowed here and borrowed exclusively before the borrow ends
 --> rename.science:9:1
  |
9 | rename(doc, doc.body)
  | ^^^^^^^^^^^^^^^^^^^^^ ...and borrowed here, exclusively
  |             -------- `doc.body` is borrowed here, shared
  |
  = 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

error[SC0333]: `local` is borrowed for longer than `local` exists
 --> dangling.science:5:5
  |
5 |     let local be Doc(title: "a")
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ...and the borrow is still needed here, after the value is gone (continues to line 6)
  |         ----- `local` is declared here
6 |     borrowed local
  |     -------------- `local` is borrowed here
  |
  = note: a borrow may not outlive what it points at (§6.1 rule 5); the value's storage ends at the close of the scope it was declared in
  = note: there is no lifetime syntax to widen: the fix is to return an owned value or an index, which is what `examples/21_compiler_shapes.science` §1 does

Both of those are printed by sciencec check today. The second note on each is the one doing the teaching: a language that has removed a syntax has to say what to write instead, because there is no annotation for the reader to reach for.

The ownership band, in full

Two checks are suppressed in a body that calls something the compiler cannot name, and both suppressions are recorded as temporary: SC0340 is not reported there, and rule 5 is not checked against a local an earlier phase could not build. A hole makes moves invisible rather than spurious, so the move check needs no such suppression — which is why it is the one rule on this page with no asterisk attached to a missing callee.

Dynamic dispatch

interface Summarize:
    def summarize(self) -> String
    def preview(self) -> String:
        self.summarize()

def describe_any(value: borrowed any Summarize) -> String:
    value.preview()

def describe_each of T(value: borrowed T) -> String where T: Summarize:
    value.preview()

The two functions do the same thing by different means, and the difference is worth knowing. describe_each is generic and monomorphised: the compiler emits one copy per concrete T, each specialised, each inlinable, and the binary grows. describe_any takes any Summarize, which is one function in the binary dispatching through a table at run time. any Interface is always used behind an indirection — a borrow or a box — because its size is not known at the call site. Monomorphisation is the default because numeric specialisation is where this language's performance is supposed to come from.

Neither half is emitted. There is no monomorphisation walk and no vtable: unsizing a borrow into an interface object is SC0400, and so is a call to a generic function. Both check. changing

Control flow#

if/else is an expression, and so is match. A block is an indented body after :, or a single expression written inline. There are exactly two loops, six words in the whole group — if, else, match, for, loop, and the three jumps break, continue, return — and the list of forms that do not exist is longer than the list that does.

type State:
    residual: F64

def converged(state: borrowed State) -> Bool:
    state.residual <= 1.0e-6

def refine(state: State) -> State:
    State(residual: state.residual / 2.0)

# The inline body ends where the EXPRESSION ends, not at the newline: the
# then-branch stops at `else`, because `else` cannot continue an expression.
def clamp(value: Int, limit: Int) -> Int:
    if value > limit: limit else: value

def count_to(width: Int, n: Int) -> Int:
    let mutable total be 0

    for i in 0..width:             # half-open: the last value is `width - 1`
        total be total + i

    for i in 0..=n:                # inclusive: it visits `n`
        if i is 3:
            continue               # skip one turn, keep the loop
        total be total + i

    total

def refine_until_stable(start: State) -> State:
    let mutable state be start

    # `loop` is the only unbounded loop, and `break` is the only way out.
    # There is no `while`.
    loop:
        if converged(state):
            break
        state be refine(state)

    state

Every form, and the exact shape of each

Two of those rows are the decision worth defending. break carries nothing out and loop has no value, so a loop is a statement in everything but its filing — where Rust writes let x be loop: … break v, Science writes a mutable binding above the loop and assigns into it. The gain is that loop needs no unification between its breaks and no type at all, so its body can be read one line at a time; the cost is one extra binding at every place a loop computes an answer, and that binding has to be mutable when the value it holds would otherwise have been final.

There is a sharp edge here and it is worth knowing before you meet it. break n parses. The operand is parsed, resolved and type-checked — it can have effects, so it is evaluated — and then its type is thrown away and the loop is () as before. So a loop written with break n in the belief that the loop yields n checks clean and yields nothing, and the mistake surfaces only if the loop sits in a position that wanted a value, as SC0525: expected Int, found (), reported against the loop line rather than against the break. Accepting the operand is deliberate — it keeps the door open for giving loop a value later without a grammar change — and the cost is that today the grammar promises something the type system does not deliver. changing

if is an expression, and elif is not a word

def band(n: Int) -> Int:
    if n > 100:
        3
    else:
        if n > 10:
            2
        else:
            1

# `else:` followed by an inline `if` is the same thing on one line, and it is
# the chain a Python reader is looking for.
def band_inline(n: Int) -> Int:
    if n > 100: 3 else: if n > 10: 2 else: 1

let value be if band(5) > 1: 10 else: 20
print(f"{value}")

There is no elif and no else if as a single construct, and the reason is that there does not need to be one: else takes a block, an if is an expression, and an expression is a legal inline block, so else: if … already is the chain. Python needs elif because its else: would force a second indentation level; Science's inline body does not. Writing elif anyway is not a friendly migration diagnostic — it is three ordinary parse errors, because elif lexes as an identifier and the parser has no idea what you meant. That is a gap in the migration band, which covers while, trait, function, println and try but not this. changing

An if with no else has type (), so it is a statement in everything but name and a let cannot take its value. The alternative — giving it T? and filling in null — was not taken, because it would make the commonest statement in any program silently produce a value, and a nullable one at that. The branches of an if that is used for its value must agree on a type exactly; there is no numeric widening between them and no common supertype.

A branch that cannot finish does not have to agree. panic returns Never, so if b: 1 else: panic("no") is an Int, and the same is true of a branch ending in return. This is the only subtyping in the language, it exists for exactly this reason, and Never is a prelude type you can write but never construct.

while is not in the language, and the compiler says so by name

error[SC0142]: the unbounded loop is written `loop`
 --> spin.science:2:1
  |
2 | while n < 3:
  | ^^^^^^^^^^^ `while` is not a keyword in Science, and `loop` takes no condition
  |
  = note: end it with the condition negated: make `if not …: break` the first statement of the body, or write a count as a range, `for i in 0..n:`
  = help: open the loop with: `loop`

A condition-driven loop is loop: with an early break, which is two lines longer. That is Go's trade and its known cost, taken for a specific reason: ranges already cover the counting case while is usually misused for, and the language would otherwise carry two forms where one does. loop while condition: was considered and held back, because it reintroduces exactly the second form this decision exists to remove — and it is source-compatible to add later if the verbosity is genuinely felt. What the decision bought immediately is the diagnostic above: because while is a reserved word rather than an identifier, the compiler can meet the habit where it happens and say what to write instead, which a language that simply lacked the word could not.

The cost that is not the two lines. loop: with the test at the bottom is a do-while, and loop: with the test at the top is a while; the reader has to look at the body to find out which, where the keyword used to say it in the first word. The design's answer is that the body is one screen and is going to be read anyway, which is true of the loops in a numerical kernel and less true of the loops in a parser.

for, its ranges, and what the loop variable owns

def total_of(xs: borrowed Array of Int) -> Int:
    let mutable total be 0

    # The binder is a pattern, so a tuple element can be taken apart here.
    for x in xs:
        total be total + x

    total

def pairs_of(ps: borrowed Array of (Int, Int)) -> Int:
    let mutable total be 0
    for (left, right) in ps:
        total be total + left * right
    total

def characters(text: borrowed String) -> Int:
    let mutable n be 0
    for _ in text.chars():         # `_` in a binder discards the item
        n be n + 1
    n

Ranges use .., never :. 0..n is half-open and 0..=n is inclusive, so for i in 0..n: is the counting loop and there is no off-by-one to memorise. The colon is not available for a slicing notation because : already opens blocks and separates match arms, fields, named arguments and bounds, and a character with five jobs cannot take a sixth. Ranges sit below everything on the precedence ladder, so 0..n - 1 counts to n - 1.

for x in xs: borrows. Iterating a collection does not consume it, and consuming is written out with iterate_consuming(). This is a deliberate correction of the single most-reported wart in Rust's collection API, where for x in v silently moves and burns every beginner once. The prelude keeps the promise: Array of T implements Iterate with Item is borrowed T, so the loop variable is a borrow, and the Copy rule is what makes arithmetic on it legal.

The element type is Iterate.next's return with its ? removed, and nothing else is consulted. The checker does not desugar the loop into a call it then re-resolves; it looks the implementation up and reads Item off it. The saving is a whole resolution round trip per loop. The price is visible when there is no implementation to read: for x in doc: over a record that implements nothing binds x at the error type and reports nothing at all, so the loop checks clean and the mistake surfaces as a confusing message somewhere downstream, or as nothing. changing

Both ends of a range are required, and there is no descending form. ..n, n.. and a bare .. do not parse: an open end would have to be told apart from a .. that ends a line, and no method in F0 takes one, because Array has no slicing. There is no step — step is an ordinary identifier you may bind — and no reversed() in the prelude, so counting down is a loop with a decrement. for i in 5..0: checks clean and describes an empty range; the parser's reversed-range diagnostic, SC0154 — this range starts at 3 and ends at 1, so it holds nothing — is aimed at the index bracket and does not look at a loop header.

Blocks are indentation, and the inline body is an expression

A block opens with : at the end of a line and is the run of lines indented past the opener; the lexer turns that into Indent and Dedent tokens, one Dedent per level closed, and the parser never sees a column number. Written inline, a block is one expression and it ends where the expression ends — if a: b else: c works because else cannot continue an expression, not because the whole thing fits on a line.

An inline body may be an expression, an assignment, or return / break / continue. It may not be a let, which would bind a name nothing could then use, and the compiler says exactly that rather than reporting a parse failure:

error[SC0109]: the body of an inline block must be an expression, and a `let` binding is a statement; write the body as an indented block instead
 --> inline.science:2:15
  |
2 |     if n > 0: let x be 1 else: 0
  |               ^^^

A dangling else binds to the innermost if, which is the only rule available once else: may follow an inline body, and it is the rule every reader already expects. Where it is genuinely ambiguous to a human, the fix is the indented form, and the formatter will write it that way.

Three things continue a line, and a trailing operator is not one of them. Inside an unclosed bracket, line breaks and indentation are ignored entirely, so a call or a list may be spread over as many lines as it likes. Outside a bracket, exactly two things continue the line above: a line beginning with ., which is how a method chain is broken up — see Chains and closures — and a line beginning with where, which is how a long signature is. Nothing else. let n be 1 + with the 2 on the next line is SC0105, expected an expression, found end of line, and the fix is a pair of parentheses. There is no backslash.

The two allowances are each one token wide, and that is the whole argument for them. A leading . counts only when a letter follows it, so .. never continues a line — a range is not a chain link. A leading where counts only when the word ends there, so a variable called whereabouts is safe, and it costs nothing because no statement may begin with where anyway. A general rule — a line ending in a binary operator continues — was not taken, because the formatter has to model every continuation rule in order to be idempotent, and a rule keyed on the first token of the next line is one the formatter can decide without looking ahead.

Indent with spaces. A tab in indentation is SC0003, not a width the lexer guesses: Science does not interpret tabs: their width depends on how the file is displayed, so a block would mean different things to different readers. An indentation that matches no open level is SC0004, and the message lists the levels that are open, which is the fact the reader needs and the one a column number does not give. And match has no inline form: its arms are always an indented block, because the arm separator is : and an inline match would put three colons on one line with no rule to tell them apart.

where is for bounds and for nothing else

interface Summarize:
    def summarize(self) -> String

interface Titled:
    def title(self) -> String

# One bound per clause, comma-separated; `where` never introduces a guard,
# a loop condition or a pattern test.
def describe of T(value: borrowed T) -> String where T: Summarize, T: Titled:
    value.title()

where attaches to a declaration and constrains a type parameter. It is not a match guard, it is not a comprehension filter, and it is not a loop condition — three jobs the word does in three other languages, which is exactly why it is worth saying it does none of them here. Two bounds on one parameter are written as two clauses, T: Summarize, T: Titled, rather than with a +: the language has no type-level operator, and inventing one for this position would be a second grammar for a list.

Divergence, the tail expression, and the hole in the middle

A function's value is its last expression; return is for leaving early. There is no implicit null return and no falling off the end into a default — a body whose tail is a statement has type (), and against a declared -> Int that is SC0525, expected Int, found (), reported at the tail. That is how a missing return is caught: not by a dedicated control-flow pass, but by the ordinary type of the body.

Which means the check is exactly as good as the tail's type, and in three shapes it is not good enough. A body whose tail is if b: return 1 — an if with no else, whose only branch diverges — is accepted against -> I64, builds, runs, and hands back whatever was in the slot when b is false. break or continue written outside any loop is accepted by every phase that runs on check, and the jump is then silently dropped. And two branches of an if need not agree with each other when nothing else said what the type should be: in let x be if c: 1 else: "a" the then-branch simply wins, x is an Int, and no diagnostic is produced. Write the expected type — let x: Int be …, or a -> Int on the enclosing function — and both branches are checked against it, one SC0525 each. changing

There is no reachability pass at all, which is the common cause of the second and third of those. Statements after a return are not reported; they are lowered into a MIR block nothing jumps to, deliberately, because skipping them would make the lowering depend on a reachability judgement it has no reason to make. The one place dead code is refused is a match arm — SC0537, in Patterns — and that one falls out of the exhaustiveness algorithm rather than from a pass written for it.

Every loop and branch form that does not exist

What of this builds, and what only checks

Every for loop above checks and none of them builds. A for lowers through range and iterator temporaries that reach the back end untyped, and sciencec build refuses to emit a value whose type is the error type: SC0400, naming a for loop's range and iterator temporaries as one of the four shapes it has met. for i in 0..10: is included. This is the single largest hole between check and build, it is a plumbing gap rather than a design question, and it is why the runnable examples on this page count with loop or not at all. changing

def double(n: Int) -> Int:
    n * 2

let mutable n be 1
loop:
    n be double(n)
    if n > 20:
        break

print(f"{n}")
# 32

That listing is the shape that runs today, and the shape of it is load-bearing. n gets its type from double's signature rather than from an integer literal, and that is what keeps it out of SC0400: a let mutable n be 0 whose only arithmetic is against other literals reaches the back end with no type at all and is refused. The workaround is a suffix — 0i64 — or a call, as here.

Patterns#

match is exhaustive, and the diagnostic for a missing case is the witness — the value nothing covers, printed as source you can paste. An arm is inline after its :, or an indented block. There are eight pattern forms, no guards, and no bindings inside an alternation.

choice Format:
    Plain
    Markdown
    Json

type Point:
    x: Int
    y: Int

choice Token:
    Symbol(Char)
    Word(String)

def name_of(format: borrowed Format) -> String:
    match format:
        Plain: "plain"
        Markdown: "markdown"
        Json: "json"

def qualified(format: borrowed Format) -> String:
    match format:                      # qualified variants mean the same thing
        Format.Plain: "plain"
        Format.Markdown: "markdown"
        Format.Json: "json"

def size_of(digit: Int) -> String:
    match digit:
        0 | 1 | 2: "small"
        3 | 4 | 5 | 6: "medium"
        _: "large"

def is_separator(token: borrowed Token) -> Bool:
    match token:
        Symbol(',') | Symbol(';') | Symbol('.'): true
        _: false

def where_is(point: borrowed Point) -> String:
    match point:
        Point(x: 0, y: 0): "origin"
        Point(x: 0, y: y): "on the Y axis"
        Point(x: x, y: 0): "on the X axis"
        Point(x: x, y: _): "general"

The eight forms, and nothing else

A bare name is a binding until resolution says otherwise. The parser cannot tell Json from other — they are the same token in the same position — so it produces a binding, and the resolver rewrites it into a variant if a variant of that name is in scope. The cost of that rule lands on a typo. A misspelled payload variant, Circl(r), is SC0200, cannot find Circl in this scope, because a bare name followed by a parenthesis cannot be a binding. A misspelled unit variant — Markdow for Markdown — is a perfectly good binding name and matches everything. Write it in the middle of a match and you get SC0537 against the arm below it, which is a true statement about a program you did not write. Write it last and the file checks clean: one arm silently answers for a case, the exhaustiveness check is satisfied by a catch-all nobody meant, and nothing is reported at all. changing

A variant may be written qualified or bare: Plain and Format.Plain are the same pattern. The bare form is what a match arm usually wants, since the scrutinee's type already says which choice is meant; the qualified form is there for when two choices in scope have a variant with the same name. A pattern's path may have several segments for exactly this reason and no other — there is no field access in a pattern, so a . inside one can only be a qualification.

Record patterns match by name, and the field you leave out is a wildcard

type Reading:
    sensor: Int
    celsius: Int
    flagged: Bool

def describe(r: borrowed Reading) -> String:
    match r:
        # `flagged` is not named, so it is not asked about.
        Reading(sensor: 0, celsius: c): "sensor zero"
        # The name left of the colon is the FIELD; the thing right of it is
        # the pattern. That is the same order construction uses.
        Reading(sensor: s, celsius: _, flagged: true): "flagged"
        Reading(sensor: s, celsius: c, flagged: false): "ordinary"

Omitting a field is the same as writing _ for it, so there is no .. rest pattern and no need for one: the rest is whatever you did not mention. That is a smaller grammar than Rust's, and it costs one thing — a record pattern does not say, by its shape, whether the author considered every field. Adding a field to a record therefore does not break any match, which is the opposite of the trade choice makes, and the asymmetry is deliberate: adding a variant is a new case to answer for, adding a field is not.

Whether the constructor is a record or a variant is decided by the punctuation, not by a lookup. Named fields mean a record, positional elements mean a variant — the same rule that decides the expression form. Get it the wrong way round and it is SC0206: Rect is a record type, so its pattern names its fields, with the declaration shown as a second span. An unknown field is SC0205.

An alternation may not bind

error[SC0201]: the binding `n` is defined more than once
 --> token.science:7:18
  |
7 |         A(n) | B(n): n
  |           - first defined here
  |                  ^ defined again here

So A(n) | B(n) is refused, and the refusal is worth the two arms it costs you. Every alternative of an alternation binds into one scope, so two alternatives that bind the same name are two definitions of it — and the alternative rule, the same name in every alternative is one binding, needs a check that the alternatives agree on its type and a lowering that knows which alternative matched. Neither exists. Refusing the shape outright is the honest version of that: the alternation is for cases you do not need to tell apart, which is what 0 | 1 | 2 and Symbol(',') | Symbol(';') are, and the moment you want the payload you want two arms anyway.

A dead alternative inside a live arm is not reported: Plain | Plain | Markdown checks clean. The usefulness algorithm asks about rows, and an arm is one row; asking about each alternative separately is a second traversal for a mistake nobody makes twice, and it was declined on that basis.

Nullable patterns, and the constructor that has no name

def label(n: Int?) -> String:
    match n:
        null: "absent"
        0: "zero"
        _: "present"

choice Format:
    Plain
    Json

def name_or(format: borrowed Format?) -> String:
    match format:
        null: "none"
        Plain: "plain"
        Json: "json"

A T? has exactly two constructors, and only one of them can be written. One is null. The other is present, and it is spelled by writing a pattern of T: there is no Some, because Some, None, Ok and Err were removed with Option and Result. So the second listing above answers for all three values of Format? with three arms and no wrapper anywhere, which is the whole point of making T? a type rather than a library generic.

The price of an unspellable constructor is paid in the diagnostic. A match over an I64? that answers only null is told that a value is uncovered and the witness printed is _ — because the compiler would have to write Present(_), and that is not a thing you could paste into an arm. It is the one place the witness cannot be source, and it is the direct cost of the syntax that makes every other nullable match read well.

And a binding arm under a nullable binds at the nullable type. In match n: null: 0 / v: v the name v has type Int? and not Int, so using it as a number is SC0525: expected Int, found Int?. The present constructor is invisible to the binder as well as to the printer. The way to get the payload is narrowing — if n?: — which is flow-sensitive and knows what a match arm does not. That asymmetry between the two ways of asking about a nullable is real and it is not designed; it is where the two features meet and have not been introduced. changing

Exhaustiveness is the whole reason choice exists

The check is Maranget's usefulness algorithm — the standard one, from Warnings for pattern matching — with one change that is the reason the diagnostics read the way they do: the recursion carries the value it found, so the answer is the witness. An algorithm that returned a yes or a no would leave the message to be assembled afterwards by something that had thrown away what it knew.

error[SC0250]: `Format` has a value no arm of this `match` covers: `Markdown`
 --> render.science:7:11
  |
7 |     match format:
  |           ^^^^^^ this is `Format`
  |
  = note: a `match` answers for every value or the program has no answer for the rest (§4.5); write an arm for `Markdown` — or a `_` arm, which covers everything the arms above leave

The witness is the message, deliberately. A diagnostic that says only "not exhaustive" makes the reader re-derive what they missed, which for a record pattern means working out which combination of fields no arm reaches. So the compiler prints uncovered values — Point(x: _, y: _), with the field names, in the shape the reader can paste into a new arm — in the declaration order of the choice. Borrows are peeled first, so a borrowed Format scrutinee names Markdown and not borrowed Markdown. The type is printed as the alias you wrote, not as its expansion.

Where the witness is coarse, and where the count stops counting

Char is finite and is deliberately treated as infinite. Enumerating a million code points to prove a match complete would be correct and useless; requiring a _ arm costs one line and is what every such match wants anyway. The same reasoning covers the integers, where it is not a choice.

The witness does not refine a literal. Given arms A(0) and nothing else over a choice of A(Int), the uncovered set is every A whose payload is not zero, and what is printed is A(_). Given Point(x: 0, y: 0) and Point(x: 0, y: y), the witness is Point(x: _, y: _). The shape is always right and the values in it are as specific as the constructor set allows, which for an infinite set is not specific at all. Pasting the witness in as a new arm therefore always fixes the error, and sometimes produces an arm you then have to narrow by hand.

Three witnesses are shown and the remainder is counted, and the count saturates. Collection stops at twice what is shown, so a choice with four uncovered variants says V1, V2, V3, and 1 more, and a choice with twenty uncovered variants also says and 3 more. That is a bound on the work rather than a count of the problem, and a reader who takes the number literally will be wrong in the one direction that is safe: there are never fewer left than it says. changing

The check gives up rather than guess, in five situations. An erroneous scrutinee type, an unresolved pattern anywhere in any arm, an alias that will not reveal, a scrutinee whose constructors cannot be enumerated — and a budget: a hundred thousand steps per match, after which it reports nothing at all. Unreachability is quadratic in the number of arms, which is what the budget is really guarding. Every one of those is a missed error rather than a wrong one, which is the direction a check whose false positives would be hated has to fail in.

And when it is silent, the fall-through is not a panic. MIR terminates the path past the last arm with an unreachable terminator rather than a trap, on the ground that deciding what an inexhaustive match does at run time is the exhaustiveness check's decision and not the lowering's. So an inexhaustive match that got past one of the five silences above is undefined behaviour and not a diagnostic. changing

A wildcard arm switches the check off, and a dead one is an error

_ switches exhaustiveness off, and that is the trade: use a wildcard where the cases are genuinely open-ended (an integer, a character) and name every variant where they are not. The difference shows up the day somebody adds a variant — a wildcard absorbs it silently, and a complete set of arms stops the build in every place that has to decide what to do about it.

And a wildcard that covers nothing is an error too. An arm no value reaches is SC0537, and there is no attribute to silence it, because an arm is checked and lowered whether or not anything reaches it — a dead one is code that cannot run and therefore cannot be found to be wrong.

error[SC0537]: no value reaches this arm
 --> render.science:9:9
  |
9 |         _: "other"
  |         ^ every value this matches is matched above
  |
  = note: an arm is checked and lowered whether or not anything reaches it, so a dead one is code that cannot run and cannot be found to be wrong; there is no attribute that silences this, so the fix is to delete the arm or to move it above the one that shadows it

There are no guards, and the replacement is an if in the arm

def size_of(n: Int) -> String:
    match n:
        0: "zero"
        # No `n if n > 100:` — the condition goes in the body, where
        # exhaustiveness does not have to reason about it.
        other: if other > 100: "large" else: "small"

Writing x if x > 3: … is a parse error — SC0100, expected :, found if — because the pattern grammar ends at the pattern and the separator has to be the next token. There is no where form either. That is an absence rather than a refusal: no note ever specified guards, so there is no diagnostic explaining them and no plan recorded for adding them. changing

The absence is load-bearing in one direction. A guard is a condition the usefulness algorithm cannot evaluate, so every language that has guards has to treat a guarded row as covering nothing — which means Some(x) if x > 0 followed by Some(x) if x <= 0 is not exhaustive and never can be. With no guards, every row in the matrix is a real row, the witness is always a real value, and the two diagnostics above are exact rather than conservative. The cost is the extra indentation level in the listing above, paid on every arm that wanted a condition.

Where a pattern may stand, and where it may not

Two positions: a match arm, and a for binder. That is the whole list. for (left, right) in ps: takes a pattern apart, and so does for _ in xs:.

A let is not a pattern position. let a, b be f() is a flat list of names, not a tuple pattern: no nesting, no literals, no variants, no _. Even let _ be f() is refused — SC0102, expected an identifier, found _. The reason is the one that runs through this whole section: a pattern in a let is either irrefutable, in which case it is a list of names wearing brackets, or refutable, in which case the language owes an answer for what happens when it does not match — and the form that can be checked for exhaustiveness is match. Keeping patterns out of let is how the language avoids owing that answer. The arity is still checked, by the type checker: SC0529, this let binds 2 names and the value is not a tuple.

A refutable pattern in a for binder is the hole that rule leaves. for Circle(r) in shapes: parses, resolves, type-checks and lowers — to an unconditional take-it-apart-and-bind, with no test. Exhaustiveness only ever visits a match. So the one position that takes a full pattern and has nowhere to put a failure is the one position nothing checks. changing

Function and closure parameters are not patterns either. A parameter is a name and a type; a closure's parameter is a name. So there is no destructuring in a signature, which keeps a signature readable as a contract rather than as an implementation detail.

Every pattern form that does not exist

Arms are tested in order, and nothing is checked against the scrutinee's type

There is no decision tree. A two-variant choice lowers to two comparisons and not one jump table, so a match is not a constant-time dispatch and a long one is a chain. That is a statement about the generated code rather than about the language, and it is here because it is observable. The reordering that would make it a tree is an optimisation nobody has written, and the order itself is guaranteed: a pattern's arms are tested top to bottom.

And the pattern is never checked against the scrutinee's type. A "hello" arm on an Int scrutinee, or a Circle(r) arm on a Format, is not a type error — there is no diagnostic code for a pattern/scrutinee mismatch, and a literal pattern is simply given the scrutinee's own type without unifying. A tuple pattern of the wrong width is silent too. What you get instead is whatever SC0250 says about the constructors that are missing, which is a message about the right match and the wrong mistake. changing

Errors#

A function that can fail returns its value and an error, and the error type is nullable. There is no Result, no Option, no try and no exception.

type Config:
    host: String
    port: U16

Config has:
    def empty() -> Config:
        Config(host: String.new(), port: 0u16)

choice ConfigError:
    NotFound(String)
    Malformed(String, Int)

ConfigError implements Error:
    def message(self) -> String:
        match self:
            NotFound(key): copy_of(key)
            Malformed(detail, line): copy_of(detail)

def copy_of(text: borrowed String) -> String:
    let mutable out be String.new()
    out.push_str(text)
    out

def parse(text: borrowed String) -> (Config, ConfigError?):
    if text.is_empty():
        return (Config.empty(), ConfigError.Malformed("empty input", 1))
    (Config(host: copy_of(text), port: 8080u16), null)

# The pair: what the function produced, and what went wrong.
def read_config(path: borrowed String) -> (Config, ConfigError?):
    let text, err be read_file(path)
    if err?:
        return (Config.empty(), ConfigError.NotFound(copy_of(path)))

    return parse(text)

The three pieces, and what each one is

T? is a nullable type — a T, or null. It replaces Option of T, and it is the spelling Kotlin, Swift, TypeScript and C# all share, so it needs no teaching. There is no wrapper: the present case is the value, which is why a body can satisfy a -> String? by producing a String, and why an exhausted iterator just returns null. It is a distinct type and not a union: T coerces into T? and T? never coerces to T, and T?? does not exist.

-> (Config, ConfigError?) is a pair, received by destructuring at the binding: let config, err be read_config(path). A function with nothing to hand back returns the error alone, because the pair would have () in its first slot and a name bound to that could do nothing.

? is a presence test and it is total. This is the piece most likely to be misread. It looks like Rust's propagation operator and it is not it: err? is a Bool, true when the value is not null. It never returns from the enclosing function, never unwraps and never fails. print(f"{pending?}") prints false or true. The character was free because the earlier design removed the propagation operator, so it now means exactly one thing.

? sits on the tightest rung, with call, index and field access, and applies to the whole postfix chain to its left. config.port? is (config.port)? and next()? is (next())?. It reads in the opposite direction from the prefix try it replaced, which covered the chain that followed it — which is why this was a rewrite of that rung and not a rename. Foo? the type and Foo? the test are different grammar positions and no production admits both.

type Override:
    host: String?
    port: U16?

def heading(text: borrowed String) -> String?:
    if text.starts_with("# "):
        text.replace("# ", "")
    else:
        null

def host_length(settings: borrowed Map of (String, String)) -> Int:
    let found be settings.get("host")
    # Inside `if found?:` the compiler knows `found` is not null.
    if found?:
        return found.length()
    0

let mutable pending: String? be null
print(f"{pending?}")                 # `?` evaluates to a Bool, never to the value
pending be "science.toml"
print(f"{pending?}")
if pending?:
    print(pending)

null and ?, as typing rules

null is a literal with no default type, and it is the only literal in the language that has none. An integer literal with nothing to constrain it falls back to I64 and a float to F64; null falls back to nothing, because no type is inhabited by null alone. So let x be null is SC0526, the type of this value cannot be inferred, and the fix is always to say which nullable it is: an annotation, a parameter, or a declared return type.

And it is the one literal that takes the whole expectation rather than its payload. Every other literal widens into a nullable — let n: Int? be 3 types 3 as Int and then widens — whereas null binds to Int? itself. That asymmetry is the point of making T? a distinct type: null inhabits the nullable and nothing else, so it is refused at every shape the checker can classify and admitted at the few it cannot. In a mismatch it is reported literally, as found null, because there is no type name to print.

e? has type Bool whatever e is. The operand is synthesised, never checked against an expectation, and if its revealed type is not nullable the result is SC0530 — this value is never absent, with the note ? tests a T? for a value; on a T it is always true. The node is still built and still typed Bool, so one mistake produces one diagnostic and not a cascade. A type the phase cannot classify — a parameter, Self — is admitted in silence, which is the direction a diagnostic about an always-true test has to err in.

T?? is SC0520, a type is nullable once, refused at the point the type is written rather than collapsed silently. The same argument one level down at the value is what SC0530 is: a construct that can only ever produce one answer is never what anybody meant.

Narrowing, exactly

Narrowing is a flow-sensitive fact about a place — a local, or a field projection from a narrowed place — and it is invalidated by any write to that place or to a prefix of it. config.port? narrows config.port and not config; writing to config invalidates it and writing to config.other does not. not err? narrows the other way round, and and narrows both operands in the then-branch.

An early return inside if err?: narrows err to null for the rest of the function, and that single rule is what makes the Go shape bearable: after the three lines that handle the failure, the compiler agrees with you that there is no failure left. A narrowing established before a loop does not survive the back edge unless it survives every path through the body, because the meet is intersection.

One dependency is worth knowing because it fixes an order: a narrowing is invalidated at the point an exclusive borrow is created, not where that borrow writes. That makes the type checker depend on a fact the region checker proves, and the two run in that order — which is why check's phase list has types before regions and not the other way about.

Which error type to name, and what each one costs

type Config:
    host: String

Config has:
    def empty() -> Config:
        Config(host: String.new())

choice ConfigError:
    NotFound(String)
    Malformed(String, Int)

ConfigError implements Error:
    def message(self) -> String:
        "the configuration could not be read"

type StartupError:
    detail: String

StartupError implements Error:
    def message(self) -> String:
        "the program could not start"

StartupError has:
    # The conversion the removed `try` used to perform invisibly. It is an
    # ordinary associated function now, and the caller writes the call.
    def from_config(inner: borrowed ConfigError) -> StartupError:
        StartupError(detail: inner.message())

def read_concrete(path: borrowed String) -> (Config, ConfigError?):
    (Config.empty(), null)

# `Error?` is shorthand for `(any Error)?`: it composes across a library
# boundary, and it boxes, which the concrete form does not.
def start(path: borrowed String) -> (Config, Error?):
    let config, err be read_concrete(path)
    if err?:
        return (Config.empty(), StartupError.from_config(err))
    (config, null)

# A function with nothing to hand back returns the error alone.
def save(path: borrowed String, text: borrowed String) -> Error?:
    let err be write_file(path, text)
    if err?:
        return StartupError(detail: "the file could not be written")
    null

Error is a one-method interface — def message(self) -> String — so Error? in a return position is shorthand for (any Error)?. The shorthand exists because the long form appears in the signature of every fallible function in the language, and -> (Config, (any Error)?) is not a signature anyone should have to read.

The choice between the two forms is real and it is the author's. A concrete error type — usually a choice — keeps match exhaustive and costs no allocation, so it is right when the caller is expected to tell the cases apart. The interface form composes across a library boundary and boxes, so it is right at the top of a program where the only question is what to print. The rule of thumb: a library exports a concrete type, an application uses Error?.

Conversion between error types is written out, at the return. There is no implicit widening — which is exactly what the removed try did invisibly by calling From, and no section of the old design ever said that it did, which is how two files in the example corpus came to depend on an unspecified conversion. Making it explicit closes that hole by construction, and the price is visible above: StartupError.from_config(err) is a call you write. What is implicit is one step and only one: a concrete error type coerces to any Error at a return and at an argument, and nowhere else.

The prelude ships two concrete error types, IoError and TextError, and three functions that produce them: read_file(path) -> (String, IoError?), write_file(path, text) -> IoError?, and String.parse_int/parse_float, which return (I64, TextError?) and (F64, TextError?).

What this costs, stated plainly

Three lines per fallible call instead of one. The call, the if err?:, and the return. This is Go's well-known tax and it is real: when the corpus file for this feature was rewritten against the new model it roughly doubled in length. The argument for paying it is that the error path is then written where it happens, in the order it happens, for a reader rather than for a writer — and the premise of the whole design is that this code is mostly read.

Nothing in a type forces the error to be read, and that is the serious one. A Result made ignoring a failure a type error; a returned Error? can be dropped on the floor, which is Go's problem and Go pays for it. The mitigation is SC0140, and it has shipped: a binding of a nullable error type that is never tested with ? before the function returns is a compile error rather than a lint.

error[SC0140]: `err` is never checked for an error
 --> load.science:5:15
  |
5 |     let text, err be load(path)
  |               ^^^ bound here and never tested
  |
  = note: test it with `if err?:`, pass it on, or return it — or rename it to `_err` to say the failure is deliberately ignored

How a binding becomes a candidate: a type test, or a position

It is a forward reachability question over the typed tree and not a full dataflow — mark every candidate binding, mark every ? that reads it, report the ones with no reader — so it is linear in the size of the body. There is deliberately no fixed point. A ? on one path is the author having thought about it; a diagnostic that demanded one on every path would fire on if urgent?: check(err) and be wrong about a program that is fine.

What makes a binding a candidate is the interesting half, and there are two answers, either of which is enough. The type test is the specified one: an E? where E is any Error, or a named type this crate declares implements Error:. The position test is the one the implementation added, and it exists because the type test, read literally, is silent on exactly the program a beginner writes — a bare choice with no implements line, returned as the second half of a pair. Conditioning the guard on a declaration the language does not require anywhere would have lost the whole point of the model on the file that needed it most.

The four conditions are conjunctive, and you can see each of them by moving one thing. let n, maybe be load() where load returns (Int, Int?) is reported, although Int implements no interface at all. Put the nullable first — -> (Int?, Int) — and it is not. Make it the only binding and it is not. Build the pair by hand instead of calling and it is not. The cost is stated rather than denied: a genuine def midpoint() -> (F64, F64?) is now reported for a nullable that is not a failure at all. Three things were weighed against it — the corpus contains no such signature across ten declarations in four files, the language gives that shape no other meaning, and the escape is one character.

The four exclusions, and the three readers nobody wrote down

choice LoadError:
    NotFound(String)

LoadError implements Error:
    def message(self) -> String:
        "not found"

def load(path: borrowed String) -> (Int, LoadError?):
    (0, null)

def handle(err: LoadError?) -> Int:
    0

# 1. Returned: the obligation goes to the caller.
def passed_up(path: borrowed String) -> (Int, LoadError?):
    let value, err be load(path)
    (value, err)

# 2. Passed to a parameter of error type.
def handed_on(path: borrowed String) -> Int:
    let value, err be load(path)
    handle(err)

# 3. Statically null: there is nothing to test.
def nothing_to_test() -> Int:
    let err: LoadError? be null
    0

# 4. A body that cannot return.
def gives_up(path: borrowed String) -> Never:
    let value, err be load(path)
    panic("stop")

# And the opt-out, which is one character.
def deliberate(path: borrowed String) -> Int:
    let value, _err be load(path)
    value

Three more readers count and the specification names none of them, each one a refusal to guess. A match on the binding counts — and notably the pass does not then ask whether the match answered for null, although the exhaustiveness check that could tell it is now built. An argument to a method whose parameter is of error type counts, and so does an argument to a method the checker could not resolve at all, because a binding passed to an unknown callee is not a binding this pass should demand a test for. And a read wrapped in a coercion or a narrowing counts, because those are nodes the checker inserted and not something the author wrote.

Deliberately ignoring a failure is spelled with a leading underscore. let text, _err be read_file(path) says so in the source, needs no grammar, and is greppable — show me every ignored error is a question reviewers actually ask. It is a literal test on the first character of the name; the resolver does not treat the underscore specially, so _err is an ordinary name that can be read, shadowed and returned like any other, and the only thing the underscore does is silence this one diagnostic. Nothing warns that a _err was used after all, because the other convention — an underscore meaning unused — is not the one this language chose. The cost is that _ as a prefix acquires a meaning it did not have.

What SC0140 cannot see

The gap is one shape wide. An error type reached through a type parameter's bound — where E: Error, with the pair arriving as a parameter rather than from a call — is a candidate for neither test, because the implementation table answers from written implementations only and there is no call to read a position off. That is the safe direction for a diagnostic whose false positives would make it hated, and it is the same direction the exclusions are written in.

Write the implements Error block when you declare the choice regardless. It is one method, message. The type test is the one that follows the value out of the pair and into the rest of the program; the position test only ever fires at the let that received it.

Where the model is straightforwardly worse

Two fallible steps inside a single method chain produce two error types, and the conversion has been relocated to the caller's return — but a chain has no return. The old model's try converted through From at exactly that point. There is no mechanism to point at yet, and the design note says so rather than writing it up as anything else.

And a second one, which is the honest reading of the whole section: the guard is a diagnostic and not a type. A Result made ignoring a failure impossible by construction — there was no way to get the value out without meeting the error. SC0140 is a pass that can be widened, can be narrowed, and has a list of exclusions that came from reading a corpus rather than from a proof. It closes the shapes that were measured, in a language whose type system could not have been asked the question. That is a smaller claim than Result's and it is the one this design can support.

What it replaces — removed, shown only for comparison

Not valid Science · removed in syntax revision 2

function read_config(path: borrowed String) -> Result of (Config, Error):
    let text be try read_file(path)
    let config be try parse(text)
    Ok(config)

Do not write this. It is kept because the shape of the change is easier to see against what it replaces. In the removed model try unwrapped an Ok or a Some and returned the failure otherwise; it was a prefix and bound the whole chain to its right, so (try f()).port needed its parentheses. Result of (T, E), Option of T, try, Ok, Err, Some and None all went together, and so did the implicit From widening try performed. The compiler recognises try where it used to stand and reports SC0155, a migration diagnostic that deliberately carries no fix: the model that replaced it turns one expression into a binding, a test and a return, and no mechanical rewrite can choose what to return.

error[SC0155]: `try` was removed with the `Result` type
 --> old.science:2:17
  |
2 |     let text be try read_file(path)
  |                 ^^^ there is no `try` in Science
  |
  = note: a function that can fail returns its value and an error: write `let value, err be f()`, then `if err?:` and return

Chains and closures#

A pipeline is mostly glue: load, reshape, filter, batch, hand to a model, collect, write. The arithmetic in the middle is somebody else's library; the part you write is the part between the libraries, and it is a chain of method calls.

interface Summarize:
    def summarize(self) -> String

type Doc:
    title: String
    body: String

Doc implements Summarize:
    def summarize(self) -> String:
        self.body.replace("\n", " ")

def headlines(docs: borrowed Array of Doc) -> Array of String:
    docs
        .iterate()
        .discard(each.title.is_empty())
        .map(each.title)
        .take(5)
        .collect()

def by_length(docs: borrowed Array of Doc) -> Array of String:
    docs
        .iterate()
        .map(doc giving doc.summarize())
        .sorted(by: line giving line.length())
        .collect()

Lazy adapters, eager terminals, and three barriers

Adapters are lazy; terminals are eager; there is no eager mode. docs.iterate().map(each.title) allocates nothing and touches nothing until a terminal pulls it, which is why it is legal over a forty-gigabyte file. Six adapters over a million rows allocate six million-element arrays eagerly and none lazily, and take(5) after a map does five units of work lazily and a million eagerly. Three adapters are barriers and buffer the whole stream — sorted(), sorted(by:) and reverse() — which is why putting a .sorted(…) before a .discard(…) sorts rows you are about to throw away. That is the one performance trap laziness leaves open, and it is a documentation problem rather than a language one.

A chain continues across lines because a line that begins with . continues the line above it. That is a lexer rule, it is one of exactly two outside a bracket, and it counts only when a letter follows the dot — so a .. never continues a line, because a range is not a chain link. Written on one line the chain needs no rule at all; the allowance exists so that the vertical form, which is how a six-stage pipeline is meant to be read, does not have to be wrapped in parentheses.

Two closure forms, and the one case that needs the second

each names the subject of the enclosing call without declaring it. It is the shorter form and the one most chains want. It is not a loop word — iteration is for x in xs, and naming a closure's subject is the only thing each does, which is why it is reserved: letting a program shadow it would make every chain ambiguous.

name giving expression declares the parameter. It is required when the parameter is used more than once, and for the one case each cannot express: nesting. In outer.map(each.inner.map(each.x)) the two each refer to different subjects and the inner one shadows the outer irrecoverably. Science rejects that rather than picking a rule:

error[SC0115]: a nested `each` would name a different subject than the `each` around it
 --> chain.science:5:29
  |
5 |     docs.map(each.title.map(each.length()))
  |                             ^^^^ this `each` is inside another `each`
  |
  = note: name the parameter instead, with the `giving` form: `outer.map(item giving item.inner.map(each.x))`

Two each in the same argument are fine — they are the same subject — so only an enclosing each is an error. Having two spellings for one idea is design debt, and it is recorded as deliberate: Kotlin and Swift carry the same debt and it has not hurt them.

There is deliberately no lambda. lambda x: x > 5 is fifteen characters, x giving x > 5 is fourteen, and each > 5 is eight — so it would be a third spelling, longer than both spellings it joined, of something the language already says two ways. But the decisive argument is not length. λ is a primary named quantity in five fields — wavelength in spectroscopy, the decay constant in kinetics, an eigenvalue in linear algebra, the rate of a Poisson process, the ridge or lasso penalty in machine learning — and in every one of them it lands in binding or parameter position, which is exactly where a reserved word cannot be worked around. let lambda be 532 and def ridge(x: Matrix, lambda: F64) have to keep compiling, and they do.

Closure bodies are a single expression. There is no multi-statement closure and no block form, which is a real limit and a deliberate one: a lambda x: followed by a newline is, in shape, a block-opening :, and the indentation grammar cannot afford a construct where : means something else. Multi-parameter closures — (acc, x) giving acc + x — are designed and not implemented: the closure node carries one optional parameter today, so reduce and accumulate cannot yet be written. changing

each is a keyword, so it cannot be shadowed and it cannot stand alone. let each be 3 is SC0102, and let x be each + 1 outside any call is SC0212: each names the subject of the call it is written in, and there is no call here. Two each in the same argument are fine — each.title.length() + each.title.length() names one subject twice — which is why the nesting rule above is about an enclosing each and nothing else.

A closure's type is an arrow, and the value's grammar is narrower than it

def apply(f: (Int) -> Int, n: Int) -> Int:
    f(n)

# The type admits any arity. `() -> Int` and `(Int, Int) -> Int` are types
# you may write today, and there is no way to write a value of either.
def call_nothing(f: () -> Int) -> Int:
    f()

def call_two(f: (Int, Int) -> Int) -> Int:
    f(1, 2)

# A closure is also a bound: `where F: (Int) -> Int` is the generic form,
# which monomorphises where the `any`-free arrow parameter above does not.
def apply_generic of F(f: F, n: Int) -> Int where F: (Int) -> Int:
    f(n)

def increment() -> (Int) -> Int:
    x giving x + 1

let doubled be x giving x * 2
print(f"{apply(doubled, 21)}")

A closure type has no keyword and is not an interface. (A) -> B is the whole notation. That is what removes Rust's Fn/FnMut/FnOnce choice from the surface — there is no trait to pick — and it is also why captures can be uniform: with no three-way classification in the type, there is nothing for a capture mode to correspond to.

The type grammar and the value grammar do not line up, and the mismatch is a real limit. A closure type takes any number of parameters; a closure value carries one optional parameter and nothing else. So (acc, x) giving acc + x does not parse, giving 3 does not parse, and reduce, accumulate and zip's two-argument forms cannot be written even though their signatures are expressible. That is the most consequential unbuilt thing in this section. changing

And the body is one expression, with no block form, which is the layout grammar protecting itself: a parameter list followed by : and a newline is, in shape, a block opener, and a grammar where : sometimes opens a block and sometimes opens a closure is a grammar the formatter cannot be idempotent over. The cost lands on exactly the closure that wanted a temporary, and the workaround is a named function.

Naming, where it differs from what you know

map, zip, reduce, collect, flatten, first, find, sum, product, group, tally and partition keep the names you already have, because familiarity is worth more than prose where the existing word is unambiguous. And collect() always returns an Array — never inference-directed, never annotated, never a turbofish. Other targets are constructors: Set.from(…), Map.from(…).

The set is closed at thirty-eight entries; Rust's Iterator has upward of seventy. A combinator earns its place by being something a working pipeline writes often, not by being expressible — a closed set containing everything expressible is not closed. for_each, inspect, filter_map, fold beside reduce, nth, cycle, peekable and dedup are each refused with a reason. mean, variance and median are wanted and are not here, because they need a dtype-promotion policy and a defined summation order, which are numerics decisions rather than iteration decisions.

What ownership does to a chain

A chain value is a borrow of its source, wearing a long type. iterate() takes a shared borrow and each adapter moves that borrow forward into itself, so let titles be docs.iterate().map(each.title) leaves titles borrowing docs, and pushing to docs before the chain is consumed is a borrow error. Put the other way round: a chain freezes its collection for its whole life, so "mutate while iterating" is a compile error rather than a rule in the manual. That is the most valuable thing ownership buys this API.

Because regions are flow-based rather than lexical, running the terminal before the mutation is not an error at all — the borrow ends at its last use. Had the language chosen lexical lifetimes, stored chains would be close to unusable. A chain is also neither Copy nor Clone and terminals take it by value, so a half-consumed chain cannot be silently observed twice.

Items that were borrowed stay borrowed all the way into collect(), and the printed type tells you: Array of borrowed Doc is a set of views into something else, Array of Doc is yours. The rule that makes this bearable is the copy-out rule — a place expression returned from a closure yields the value when its type is Copy and a borrow otherwise — so .map(each.weight) on an F32 field gives F32 and .map(each.title) on a String field gives borrowed String. The escape is one link: .owned().

In F0 a chain cannot cross a function boundary. Writing -> MapOver of (Keep of (ArrayIterate of Doc, …), …) in a signature is not a language anyone should ship, so a function returns a collection and materialises with .collect(). That costs one allocation per boundary, and the boundary is where a pipeline wants something concrete anyway: what you hand to the next stage is a dataset, not a recipe. Libraries return named source types; user functions return collections.

Calls always take parentheses, including when they take no arguments: text.length(), never text.length. The parenthesis-free form reads better in a chain and was considered; once functions are values, doc.summary is ambiguous between calling it and naming it, and a language cannot resolve that by guessing. Parentheses mean call; their absence means a field.

What of this exists

The Iterate interface exists; the chain vocabulary does not. The prelude declares Iterate with its Item and next, and implements it for Array of T at Item is borrowed T and for Chars at Item is Char. What it does not declare is a single adapter: no iterate(), no keep, no discard, no collect, no Set. The listings above resolve because each, giving and method-call syntax are real and a prelude type's method set is open — a name the table does not have means "not written down yet" rather than "no such method". So a chain checks, and the names in it are design. changing

Read that openness precisely, because it is the one thing on this page that could mislead you. xs.flurble() on an Array checks clean; d.flurble() on a record you declared is SC0532, Doc has no method flurble. The openness is a property of prelude types only, and it exists so that a table which is admittedly incomplete does not reject programs the language will accept. The consequence for a reader of this section is that a misspelled adapter is not a compile error today, and a correct adapter is not a working program either.

What is written down is small and worth knowing, because it is what a program can call today. Array of T has new, push, get, length and is_empty — and get returns (borrowed T)?, so the index that might miss is the one that hands back a nullable. Map of (K, V) has new, insert, get, contains, remove, length and is_empty — contains rather than has, because has is a keyword. String has thirteen of the nineteen its design gives it, Chars has none at all, and Box of T has new and nothing else. There is no Set, no Range, no Lines and no Split — which is why six of String's nineteen are missing: three of them return a type that does not exist.

Array.pop is deliberately absent, and the reason is the discipline this whole section runs on. The design names it and gives it no signature. Deciding whether it returns T or T?, and what it does when the array is empty, would settle a language question in a table nobody reads, on the evidence of one call site. So it is not there. The same argument keeps mean, variance and median out of the chain vocabulary: they need a dtype-promotion policy and a defined summation order, which are numerics decisions rather than iteration decisions.

Four free functions and one that has no signature. The prelude exports print, write, panic, read_file and write_file. The last three have signatures — panic(message: borrowed String) -> Never, read_file(path) -> (String, IoError?), write_file(path, text) -> IoError?. print and write have names and no signature at all, so the arity is checked and the argument's type is not: that print is unary is a fact about the call, and that its argument must be printable is a fact about the value that nothing below the type checker can carry. changing

Map deliberately implements neither Iterate nor Index, and the reason is a good example of the discipline: Map of (K, V) implements Index of K would be an indexing operation that panics on a key that is not there, and declaring it would be deciding what m[k] does on a miss in a file nobody reads. Walking a map today goes through an Array of its keys.

The one thing you can write today that iterates

type Counter:
    seen: Int

# `Iterate` is one associated type and one method, and it is the whole
# interface. `for` reads `Item` off the implementation directly — it does
# not desugar into a call it then re-resolves.
Counter implements Iterate:
    type Item is Int

    def next(mutable self) -> Int?:
        self.seen be self.seen + 1
        self.seen

def count_three() -> Int:
    let mutable total be 0
    for value in Counter(seen: 0):
        total be total + value
        if total > 5:
            break
    total

next returns Self.Item?, and the exhausted case is null. No Option, no sentinel, no separate has_next. That is the clearest single payoff of making T? a language type rather than a library generic: the most-implemented interface in any language ends up with one method whose signature needs no wrapper.

It checks and it does not build, for the same reason every for does — the loop's next call reaches the back end unresolved, because the typed tree has no field to record the method the checker already found. The seam is one field wide and there is a test in the workspace written to fail on the day it is filled. changing

Foreign code#

Essentially every floating-point operation that matters in scientific computing already lives in a C or Fortran library somebody else tuned. dgemm is thirty years of hand-written assembly per microarchitecture. A language that cannot call these is not a scientific language, whatever its type system can prove.

The design goal is one sentence: make the boundary narrow, explicit and checkable on the Science side, and be honest that the C side cannot be checked at all. A declaration records a claim; the compiler verifies the half of the claim that lives in Science; unsafe marks the half that does not; and a hand-written safe wrapper is where the unverifiable half is discharged by an argument a human wrote down.

This is the one part of the language that is end-to-end today. A declaration, a call, an object file, a linker and a running program:

unsafe extern "C" library "c":
    def putchar(c: I32) -> I32

# `unsafe:` is a block, and it is as small as the call it wraps.
let h be unsafe: putchar(72)
let i be unsafe: putchar(105)
let stop be unsafe: putchar(10)
# Hi

type Hid is I64

unsafe extern "C" library "openblas" via pkg-config "openblas":

    type CblasLayout is CInt
    type CblasTranspose is CInt
    type BlasInt is I32

    const CBLAS_ROW_MAJOR be 101 as CblasLayout
    const CBLAS_COL_MAJOR be 102 as CblasLayout
    const CBLAS_NO_TRANS be 111 as CblasTranspose

    def cblas_dgemm(
        layout: CblasLayout,
        transpose_a: CblasTranspose,
        transpose_b: CblasTranspose,
        m: BlasInt,
        n: BlasInt,
        k: BlasInt,
        alpha: F64,
        a: ffi.Span of F64,
        lda: BlasInt,
    ) symbol "cblas_dgemm"

unsafe extern "C" library "hdf5":
    static H5T_NATIVE_DOUBLE_g: Hid
    union H5R_ref_t: size 64 align 8

Five item forms, and each earned its place against a real library. def declares an undefined symbol resolved at link. type … is … spells a C typedef. const … be … as … transcribes a #define or an enumerator. static names an exported data symbol: HDF5's H5T_NATIVE_DOUBLE is not a constant — the header defines it as (H5open(), H5T_NATIVE_DOUBLE_g) — and CPython has 199 such globals. union is an opaque blob of a known size and alignment, which is the normal path for a C union rather than an unpleasantness that does not arise. symbol decouples the Science name from the linker name.

symbol exists because of the worst FFI bug in scientific computing. BLAS and LAPACK ship in two incompatible builds — 32-bit integers and ILP64 — with identical function names, identical argument counts and identical semantics, differing only in the width of eight of dgemm's thirteen arguments. Link the wrong pair and the result is not a crash: it is correct answers for small matrices and silently wrong answers for large ones. The ILP64 builds that matter ship distinct symbols, so naming them separately turns a wrong answer at run time into an undefined symbol at link time. Where a vendor ships ILP64 under the same names — Intel MKL does — nothing can detect the mismatch, and the binding has to say so in a comment, because that is the only warning available.

How the library is found and linked

# Static, because this build is vendored and must not be swapped underneath.
unsafe extern "C" library "openblas" kind static:
    type BlasInt is I32
    def dgemm(n: BlasInt) symbol "dgemm_"

# Optional, and loaded on first use: a program that can use a GPU still
# starts on a node without one.
unsafe extern "C" library "cudnn" when available:
    type CudnnStatus is CInt
    def cudnnCreate(handle: ffi.OpaqueHandle) -> CudnnStatus

# An extern block is not a namespace. `BlasInt` above is an ordinary
# module-level name, so the ILP64 declarations — which need `BlasInt` to be
# `I64` — belong in a second module, not a second block in this one.

via pkg-config "openblas" replaces the whole search-path chain for that block with the output of pkg-config --libs. This is the only thing that gets BLAS right across machines: the correct flags are -lopenblas on one machine, -lblas -llapack on another, and five MKL libraries on a third, and no amount of source-level cleverness decides between them. HPC sites ship .pc files precisely so that this works. It is not universally available — notably on Windows — so a block using it must still name a plain fallback library.

kind static forces static linking; dynamic is the default, and the reason is specific to this audience: cluster module systems work by swapping the shared object under a fixed name, so statically linking OpenBLAS defeats the mechanism the cluster administrator is relying on.

when available changes how the whole block is lowered: instead of direct declarations the compiler emits a lazily initialised table of function pointers populated on first use, and every call becomes an indirect call through it. The block gains an is_available(). The cost is one load, one branch and one indirect call per foreign call — noise against a dgemm, not noise against a per-element function, which is why it is opt-in rather than the default.

The last comment in that block is a fact, not a stylistic note. An extern block does not open a namespace: its items land in the enclosing module, so declaring BlasInt twice in one file is SC0201, "defined more than once". Two integer widths for one library means two modules.

The interface is the wrapper, not the declaration

type Matrix:
    rows: Int
    columns: Int
    data: Array of F64

Matrix has:
    def empty() -> Matrix:
        Matrix(rows: 0, columns: 0, data: (Array of F64).new())

choice BlasError:
    Shape(Int, Int)

BlasError implements Error:
    def message(self) -> String:
        "the inner dimensions disagree"

unsafe extern "C" library "openblas" via pkg-config "openblas":
    type CblasLayout is CInt
    type BlasInt is I32
    const CBLAS_COL_MAJOR be 102 as CblasLayout
    def cblas_dgemm(layout: CblasLayout, m: BlasInt, a: ffi.Span of F64) symbol "cblas_dgemm"

# The declaration is not the interface. This is: a check a human wrote, then
# the smallest possible `unsafe` block, and no `ffi` type in the signature.
def multiply(a: borrowed Matrix, b: borrowed Matrix) -> (Matrix, BlasError?):
    if a.columns is not b.rows:
        return (Matrix.empty(), BlasError.Shape(a.columns, b.rows))

    let mutable result be Matrix.empty()
    unsafe:
        cblas_dgemm(
            layout: CBLAS_COL_MAJOR,
            m: a.rows as BlasInt,
            a: a.data.span(),
        )
    (result, null)

Why the block is unsafe at all. An extern declaration is a claim about code the compiler will never see: that a symbol of this name exists, that it takes these arguments in this order with these widths, that it does not retain the pointers it is given, that it does not free them. None of that is checkable. Writing the declaration is therefore itself the unsafe act, and the keyword belongs where the act is. Rust reached the same conclusion in its 2024 edition after a decade of extern blocks that looked safe.

What unsafe does not suspend is the part worth reading, because it is the part users of other languages assume is suspended. Type checking, trait resolution, ownership, borrow checking, region inference, overflow checks, bounds checks and exhaustiveness all still apply. unsafe means one narrow thing: the compiler's model of memory it can see is intact, and what you are about to do involves memory it cannot see. If an unsafe block is long, the binding is written wrong.

Named arguments are permitted at a foreign call site, and nowhere else in the language outside record construction. The reason is domain-specific and decisive: cblas_dgemm takes thirteen arguments, two of which are transposition flags that look identical, and confusing them produces a wrong answer rather than an error. This is the call every numerical Science program makes, and it has to be readable by someone checking a formula against a paper. Two call conventions in one language is design debt, and it is recorded as deliberate.

ffi.Span of T is a pointer and a length. At the ABI only the pointer crosses; the length exists on the Science side alone, for one reason — so that the wrapper's precondition, that lda * n does not exceed the buffer, is an expression the compiler type-checks rather than a comment. It is the raw material for a check, not the check itself.

The aliasing rule BLAS states in its own documentation — "C must not overlap A or B" — turns out to be the rule the borrow checker already enforces. A wrapper taking two shared borrows and one exclusive one makes gemm(a, b, a) a borrow error, caught by machinery that exists for reasons unrelated to FFI — and unlike most of this page, that machinery runs today. Likewise a handle type with a Drop implementation: C's "call the destructor exactly once" is Science's ownership, so a cudnnHandle_t wrapped as a handle is destroyed exactly once, on every path out including early returns, at a program point the compiler can name. There is no goto cleanup and no way to forget one.

What cannot be checked, as a list

Written as a list so that a reader can see whether their problem is on it. Retention — that the callee does not keep a borrowed pointer past the call — is unstatable and unverifiable, and the borrowed keyword in an extern declaration is the assertion. Bounds — that m, n, k, lda are consistent with the buffer — is the single largest unverified surface in the design. Internal aliasing, because noalias is emitted on the strength of the declaration. Signature agreement with the real header. Reentrancy through C. setjmp/longjmp across Science frames, which skips every destructor and is undetectable. A library calling exit. Bitfields and variadics.

And the largest practical risk, which is about linking: the linker checks that a symbol exists and nothing else. C object files carry no type information, so a wrong argument count, integer width or struct layout links cleanly and corrupts the stack at run time. The first implementation therefore refuses by-value aggregate arguments entirely and requires pointer-to-aggregate, because BLAS, LAPACK, HDF5, cuDNN and MPI pass aggregates by pointer anyway — a restriction that can be lifted source-compatibly later. F16 and BF16 may not cross by value because C has no agreed by-value ABI for half precision: _Float16 is passed differently by GCC, Clang and MSVC. That wart is felt exactly where it hurts most, in mixed-precision training, and the alternative is an ABI that is right on one compiler and silently wrong on another.

Both of those refusals have codes of their own — SC0429 and SC0431 — and neither is what you will see. The renderers exist and need a span to print; what reaches the refusal is a call site inside a body, so the message arrives as SC0400 carrying the same sentence. The day the refusal carries a span the two collapse into one. It is a small thing and it is the kind of small thing a reference gets wrong by copying a table.

Fortran is declared "C". Its difference is not the calling convention but the argument passing, which is expressed in the types, and the trailing-underscore symbols are handled by symbol "dgemm_". There is a genuine prize there: Fortran declarations carry INTENT(IN), INTENT(OUT) and INTENT(INOUT), which is precisely the borrowed / out-parameter / mutable borrowed distinction C headers lack, and LAPACK's doc comments state each array argument's dimension in a fixed machine-parseable format for 1,700 routines. That is the span length, in the source, for 1,700 routines — available only because somebody wrote the annotations down thirty years ago.

State: the block grammar, all five item forms, the three link modifiers, symbol and the closed ffi module all parse and resolve, and a def in a block is declared, called and linked — the putchar listing at the top of this section is a program that runs. from p, with errno, move ffi.CBuffer and the crate "…" clause for linking Rust are designed and not parsed. An undefined symbol at link time is SC0461, with the linker's own output quoted verbatim. changing

Tools and schemas#

tool declares a callable exposed to a model. It is a second function-declaration form, and it exists because it carries obligations a def does not — every one of which a compiler can check.

choice LineShape:
    Gaussian
    Lorentzian
    PseudoVoigt

type Peak:
    centre: F64
    width: F64

## Fit Bragg peaks in a window of flight time.
##
## Uses the run's own dark-current subtraction. Fails if the window holds
## fewer than 32 channels, because the fit is then underdetermined.
tool fit_peaks(
        ## The run identifier, as printed in the run log.
        run: String,
        ## Lower edge of the window, in seconds from the pulse.
        window_lower: F64,
        ## Line shape to fit. PseudoVoigt is the usual choice.
        line_shape: LineShape,
        ## At most 32; the fit is underdetermined above that.
        max_peaks: U8) -> Int:
    0

## Expose the same computation to a human caller.
def helper(run: borrowed String) -> Int:
    run.length()

The thesis is that the schema is the signature. Every other way of exposing a function to a model writes it twice — once as a handler the compiler checks and once as a JSON Schema nothing checks — and the two copies sit next to each other inviting a reader to believe they agree. When they drift, the failure is invisible: the schema says a parameter is a string, the handler indexes it as a list, and the model is told something false about a function it is deciding whether to call. Here there is no second artefact and therefore nothing to drift from.

Why a keyword rather than a marker. A marker that changes nothing is an attribute, and a language should not spend a word on an attribute. tool earns one because it has five obligations def has not, and a compiler checks every one: every parameter type must survive a round trip through JSON Schema; it may not be generic; no parameter may be borrowed; it must carry a ## description; and its return type is constrained. Two more come from where it may stand — module level only, and never with a self receiver.

Each of those is an argument rather than a rule. Not generic, because the list a caller is given is flat and concrete with one schema per entry, so there is nothing for T to be instantiated at. Not borrowed, because there is no caller to borrow from: the arguments were built from what arrived a moment ago and the tool is the only owner there is. Not a method, because a tool is called by name alone and there is nothing for self to be bound to.

error[SC0192]: a `tool` owns its arguments
 --> tools.science:1:23
  |
1 | tool count_rows(rows: borrowed Array of Int) -> Int:
  |                       ^^^^^^^^ there is nothing here to borrow from
  |
  = note: a tool's arguments are built from what the caller sent, so the tool is the only owner there is
  = help: take the value: delete `borrowed`

The description is mandatory, and only here

A tool with no ## run above it is SC0190, an error, and one whose summary line is blank is SC0195. This is the only construct in Science for which documentation is mandatory, and the justification is deliberately narrow, or it becomes "document your code", which a compiler has no business enforcing. Everywhere else a doc comment is read by somebody who has already decided to call the function. Here it is read by the caller in order to decide, so the string is an argument rather than prose — and the failure it prevents is invisible: an undescribed tool does not fail, it is simply never chosen, and no test catches that.

error[SC0190]: a `tool` is declared with a description
 --> tools.science:1:1
  |
1 | tool fit_peaks(run: String) -> Int:
  | ^^^^ this `tool` has no `##` comment above it
  |
  = note: the description is what a model reads in order to decide whether to call the tool, so it is program data and not documentation
  = note: an undescribed tool does not fail: it is simply never chosen, and no test catches that

There is no help line on that one, and the absence is deliberate rather than an omission. The fix is a sentence about what the tool does, and there is no mechanical replacement text a compiler can write on the author's behalf. SC0192 above does carry one, because deleting a word is a rewrite a machine can perform.

What the compiler emits

$ sciencec tools --json fit.science | python -m json.tool

[
  {
    "name": "fit_peaks",
    "inputSchema": {
      "type": "object",
      "properties": {
        "run": { "type": "string" },
        "window_lower": { "type": "number" },
        "line_shape": {
          "type": "string",
          "enum": [ "Gaussian", "Lorentzian", "PseudoVoigt" ]
        },
        "max_peaks": { "type": "integer", "minimum": 0, "maximum": 255 }
      },
      "required": [ "run", "window_lower", "line_shape", "max_peaks" ]
    },
    "description": "Fit Bragg peaks in a window of flight time.\n\nUses the run's own dark-current subtraction. Fails if the window holds\nfewer than 32 channels, because the fit is then underdetermined."
  }
]

sciencec prints that on one line; the pipe through a formatter is this page's, not the compiler's. Three things in it were derived and not written. max_peaks: U8 alone produced "minimum": 0, "maximum": 255 — the bounds are the type's width, and no other tool SDK's int can say this. A choice whose variants carry no payload became a string enum, which is the largest single win in the mapping: the model gets the complete list and does not guess, the body matches on it exhaustively, and adding a fourth line shape updates the schema in the same edit, because they are the same declaration. And the ## run became description, because a doc comment is trivia to the lexer but is carried on the token it documents rather than discarded.

One thing in that listing did not reach the schema, and it is visible by its absence. The four per-parameter ## comments are attached, preserved and dropped: no property carries a description. The protocol has a place for them and the walk does not emit them, which matters more here than a missing field usually does — the per-parameter sentence is exactly the part a model reads to decide what to send. changing

The mapping's honest edges. U64 gets a minimum and no maximum, because 2⁶⁴−1 is not exactly representable as a JSON number and emitting it would be a lie about what the other side can send. F32 and F64 both become {"type":"number"}, so the wire is wider than the type. A T? parameter is its payload's schema with the name left out of required, because JSON's "absent" and "present and null" are two states Science has one of, and the language does not pretend otherwise. NaN and the infinities cannot be written in JSON at all, so a tool taking an F64 takes a finite one and the schema cannot say so; no mitigation is proposed, and it is recorded as a limit of JSON rather than of Science.

A type the pass cannot map is reported as a gap rather than an error — the property is emitted empty, the name is dropped from required, and an "x-science-unmapped" array names it. --all-functions runs the same walk over every top-level function; it is a measurement of the type mapping and deliberately not a default, because a file's functions are not a list of callables until somebody has said which ones are. In a script that flag now lists main, which is the generated one and which nobody wrote: a small, real cost of implementing script mode as a desugaring.

prompt and agent stay reserved and unspent, and using either in declaration position is SC0196 rather than the generic "reserved for a later phase" — a phrase that reads, to anyone who knows what a compiler phase is, as though a later pass will accept it. prompt fails the test tool passes: prompt arguments in the protocol this targets are not schematised at all — a flat list of name, description and a required flag, with no types — so a prompt declaration would have no schema to derive and no drift to prevent, which leaves a function that returns a list of messages, which is a function.

Toolchain#

Seven commands, no configuration, no plugins. A file argument to check, build or resolve is the entry of a crate, and the directory it sits in is the crate root.

There is no run and no test. Dumps go to stdout, diagnostics and the 3 errors, 1 warning summary to stderr. Exit 0 when nothing was reported as an error, 1 when something was; warnings alone do not fail, so a CI job can gate on the exit code without arguing about lint levels. A file that cannot be read is an error like any other: it is reported, it sets the exit code, and the remaining files are still checked. There is no colour, so NO_COLOR is honoured trivially — the UI suite compares diagnostic text byte for byte, and escape codes in the driver would mean re-rendering diagnostics somewhere other than where they are rendered.

build writes beside the source and not into the working directory, which is the one place it differs from cc and rustc. The working directory is an environment-dependent input, and sciencec build examples/hello.science would otherwise put the executable somewhere that depends on where you were standing. The cost is that a build writes into the source tree, which is the wrong default the day there is a target/ directory to write to instead — and there is no package manager yet, so there is not one.

build needs a backend compiled in. The default build of sciencec reports SC0400 naming the feature and the install command; cargo build -p sciencec --features llvm produces the one that links. The backend binds LLVM-C dynamically, so LLVM's bin directory has to be on PATH or the compiler will not start — before main, with no diagnostic, which is the platform's behaviour and not the compiler's.

Why the formatter refuses a broken file

$ cat ugly.science
type Doc:
    title:String



def  main2( ):
    let  x be   1
    print( f"{x}" )
$ sciencec fmt ugly.science
type Doc:
    title: String

def main2():
    let x be 1
    print(f"{x}")

fmt writes to stdout unless --write is given, and it refuses any file that does not already lex and parse. That refusal is the whole safety property: reformatting a file whose token stream is a guess is how a formatter eats a program. It requires syntax and deliberately not resolution, because a formatter works on syntax and a file importing modules that are not present is still a well-formed program. It also reads exactly the files it was named and never a module one of them imports: rewriting a file the user did not ask about is not something a use line should be able to authorise.

The formatter is why one spelling per operation matters. The earlier design carried both a word form and a symbol form for all six comparisons and called the duplication debt worth taking. It was not: a formatter cannot canonicalise between a == b and a is b, because the choice depends on the operands' types, and a formatter that must run after type checking is not a formatter. The two spellings were permanently un-normalisable, which for a language whose code is largely machine-written means permanent drift. One spelling each cannot drift, and removing the second form took five words off the reserved list as well. The same argument is what refuses comprehensions.

The formatter owns the only two diagnostics in the language that a compiler can never produce: SC0900, the formatter finding that its own output does not parse back to the program it was given, and SC0901, an unmatched # fmt: off. They live in a band, SC0900–SC0999, that the core spec's table does not have — it was recorded in the design index after the formatter had already taken two codes with no band to take them from, and it still needs ratifying. A complaint from a program that reads Science is not a complaint from one that compiles it, and filing it under a compiler phase would make the phases mean less.

Doc comments, and why they survive the lexer

A run of ## immediately above a declaration is a doc comment. Unlike an ordinary # comment it is carried on the token it documents rather than discarded, so it survives into the syntax tree and onward to anything that reads a signature — which is how tools --json produces a description nobody wrote twice. This has to happen in F0 and it cannot be retrofitted: once the lexer discards them, every tool downstream is built assuming they are gone. The consumers — a documentation tool, help(), doc tests — are F1. The preservation is not.

A ## run may attach to a module, a function, a method, a type, a choice, an interface, a type alias, a const, a field, a variant, or an implements block. A run attached to nothing — at the end of a file, or separated from the next declaration by a blank line — is SC0176, a warning whose fix is "make it #". The content is Markdown and the first line is the summary; there are deliberately no @param or @returns tags, because the parameter list is already in the signature and a tag duplicating it is a second copy to drift.

The composition with ordinary comments is the part a docstring form cannot manage. # TODO next to a doc comment is an ordinary comment and does not become documentation. And a docstring would only ever cover functions: a record field, a choice variant, a const, a type alias and a module all want documenting and none of them has a body to put a string in. A docstring in a compiled language would also be an expression statement with no effect that the compiler silently treats as metadata, which is the one thing the language refuses to do anywhere else — resolve an ambiguity by guessing.

Reference tables#

Comparisons

Words for identity, symbols for order, one spelling each. == is a programming convention, not a mathematical one, and the languages that have it disagree about what it means for objects; is says what it means. >= is four hundred years old and every reader of a paper already reads it, so replacing it with is at least would have been the language going further into English than English goes. is not is the one sequence the parser assembles; is followed by anything else is equality.

Precedence, tightest first

1. 01call · index · field access · ?postfix, left to right
2. 02- not borrowedunary
3. 03as
4. 04**power, right-associative
5. 05* / % @@ is matrix multiply
6. 06+ -
7. 07<< >>
8. 08&
9. 09^
10. 10|
11. 11is · is not · > < >= <=
12. 12and
13. 13or

Assignment is absent because it is a statement, not an operator. Ranges sit below everything, so 0..n - 1 counts to n - 1. Rung 01 is the row the presence test joined: ? replaced the prefix try, which bound the whole chain that followed it, so the two read in opposite directions and this was a rewrite of the rung rather than a rename. Of the operators on rungs 04, 05 and 07, **, @, integer /, % and both shifts are parsed, typed and refused by the back end; the ladder is the language's and not this build's.

Blocks and line continuation

type Doc:
    title: String

def names_of(docs: borrowed Array of Doc) -> Array of String:
    # A line continues when the next line begins with `.`,
    # which is how a chain is broken.
    docs
        .iterate()
        .map(each.title)
        .collect()

# ...and when it begins with `where`, before a signature's bounds.
def largest of T(items: borrowed Array of T) -> (borrowed T)?
        where T: Ord:
    items.get(0)

# A line ending inside an unclosed bracket continues too, which is what
# makes an argument list breakable.
def widest(
    docs: borrowed Array of Doc,
    limit: Int,
) -> Int:
    limit

. and where are the whole list, and it is meant to stay that way. A line break is otherwise the end of a statement, and a reader should not have to look ahead to know whether it was. Inside unclosed parentheses or brackets, newlines and indentation are ignored entirely, which is the third case and the one every language has.

Blocks are delimited by indentation, spaces only. A tab in the indentation is SC0003 with no attempt to interpret it. Blank and comment-only lines take no part. Indentation matching no open level is SC0004. Comments run from # to end of line; there are no block comments. Trailing commas are allowed in every bracketed and parenthesised list. A byte-order mark is SC0001: it is not an indentation character, it is not a letter, and guessing that it was meant to be invisible is a guess.

Modules

use text.parser
use text.parser (Token, lex)

public type Doc:
    title: String

public def title_of(doc: borrowed Doc) -> borrowed String:
    doc.title

This block is a fragment, and it is worth saying why: a use line names a module that has to exist, and a single pasted file has no sibling to name. Run on its own it is SC0202, "there is no module text in the crate root", which is the resolver doing its job rather than the sample being wrong. The diagnostic goes further than it used to, because use now loads files: it names the two filenames it looked for and lists the modules the crate root does have.

A file is a module; a directory with mod.science in it is a module containing its siblings. There is no mod declaration to write, which is why mod is reserved even though it declares nothing — the word already means something, and a program using it as a name would have to be rewritten the day a declaration form arrives. A mod.science is never an entry, so top-level statements in one are always SC0213.

Reserved words

Held for later phases — using one is an error

Deliberately not reserved

The first list is the lexer's, word for word. Reserving costs nothing now and breaks every program using the name later, which is the whole argument for a list this long — but the second list has a known price and this audience pays it. shape, model and tensor are reserved globally, so x.shape and let model be … do not compile. That was accepted deliberately, so that the tensor and agent phases are guaranteed their syntax; the alternative considered was making them contextual keywords recognised only in declaration position. You will meet it the first time you try to name a parameter shape.

The third list is free on purpose: grad, dim, dims, axis, device, dtype, unit and alias are each a common variable name in the code of the people this language is for, and that outranks the convenience of reserving them. f and r are not reserved either, although they are string prefixes: the prefix is recognised only immediately before a quote, so let f be 1 stays legal. Note that where is reserved, so you cannot define a function of that name, which NumPy users will reach for.

Two words moved recently, and both moved into the first list. function left every list and is now an ordinary identifier — a program may bind it, name a field function, or write def function(…) — because the parser recognises the old declaration positionally, and a contextual test costs one line of lookahead where a reservation would cost an identifier the audience uses. tool went the other way, from "reserved for later" to a declaration keyword, because it now checks five things a def does not; a marker that changed nothing would have stayed a reservation. A word the language removed is still recognised where it used to stand and reported as a migration rather than as a stray name: SC0156 for function, carrying def as an applicable fix, and SC0155 for try, carrying none on purpose.

Diagnostic bands

The second types band was added when the first ran out. Fifty codes for types and traits was wrong by an order of magnitude — it is the largest error class in any language with a type system, and ten design notes had claimed from it before the checker was written. The band is appended rather than the table repartitioned, because renumbering codes that are already implemented and already asserted in the UI tests would buy nothing. A code's band says which phase owns it; it does not say when the band was drawn.

Six code collisions have been found so far, and every one of them was invisible to the note that caused it, because each had honestly checked against everything that existed when it started. Two of the six were worse than a collision: they were a conflict somebody had already resolved, in a file the allocation table did not reach. That is now the expected failure rather than a surprising one, and the table is scanned against itself rather than read.