Correctness

What twill's two central claims mean, how each is tested, and where each one stops. The claims are that grad computes the derivative and that the shape checker reports only real mistakes. Both are tested here against something other than themselves.

Every number below is regenerated by:

go test ./internal/tensor/  -run TestGradient -v -count=1
go test ./internal/checker/ -run TestChecker  -v -count=1

1. Gradient checking over the full operator set

What is checked

Every differentiable operator in internal/tensor, in 105 cases covering the broadcasting regimes, both axes of a non-square matrix, and the combinations where a bug shows up only in composition. The list is not maintained by hand. TestGradientCheckCoversEveryOperator parses the package's own source with go/parser, collects every exported function that takes or returns a *Tensor, and fails if one has neither a gradient-check case nor an entry in nonDifferentiable saying why it has none.

That closure property is the difference between "the full operator set" as a claim and as a fact. A new operator cannot be added without someone deciding, in writing, whether it carries a gradient.

Current coverage: 64 differentiable operators checked, 31 declared non-differentiable, 95 exported in total.

The non-differentiable list is not a way of quietly excusing operators. It holds the index-valued ones (argmax, argmin, argsort, argtopk, whose outputs are positions, integer and locally constant), the boolean comparisons, the two quantisers (QuantizeI8 and QuantizeI4 are step functions, though the gradient through the product they produce is checked), Cast, and the shape and dtype helpers that are not operators at all.

The method

For a case producing out = op(x), the harness differentiates the scalar

L(x) = sum(w * out)

for a fixed deterministic cotangent w, and compares reverse mode against a Richardson-extrapolated central difference:

D(h) = (L(x+h) - L(x-h)) / 2h            truncation O(h^2)
D*   = (4*D(h/2) - D(h)) / 3             truncation O(h^4)

Three details are load-bearing.

The cotangent is not all ones. An all-ones w makes an entire class of index-shuffling bugs invisible, because a permutation of the output has the same sum as the output. Every transpose, flip, roll, sort, gather and concat case would pass while scattering its gradient to the wrong elements. w is sin(1.7i + 0.3) * (1 + 0.25(i mod 5)): deterministic, no seed to get out of step, and irregular in sign and magnitude.

The extrapolation is what makes a tight tolerance honest. A plain central difference at the best available step carries roughly 1e-10 relative error in f64, which is close enough to a real small-magnitude gradient bug that a failure would be ambiguous. D* lands near 1e-12, so a disagreement above 1e-7 is a defect and not the difference method breathing. Measured error across the cases runs from 1e-13 to 1e-11, leaving four orders of headroom over the observed noise floor.

The step is scaled to the point, h = 1e-4 * max(1, |x_i|), so a coordinate of size 1000 is not probed with an absolute step its own rounding swallows.

Where finite differences cannot adjudicate, and what is done instead

relu, abs, clip, maximum, minimum, max, min, median, sort, topk, cummax, cummin and maxpool2d are piecewise. At a kink the derivative does not exist, and a central difference straddling one reports the average of the two one-sided slopes, which is not what any autodiff system returns. Reporting that as a defect would be reporting a property of the difference method.

So every case for a piecewise operator is sited away from its kinks: nothing near zero for relu, nothing near a bound for clip, no ties in any comparison or ordering. The kinks themselves are then asserted directly in TestGradientKinkConventions, because the convention twill picks is a decision and should be a stable one:

Three of these differ from PyTorch. None is wrong: the subgradient at a kink is a set, and any element of it is defensible. They are written down so that changing one is a deliberate act rather than a regression nobody notices.

The result

All 105 cases agree. Worst relative error by case, highest first:

composite/mlp-layer is two orders above the rest and is not a defect. It is a softmax over a tanh over a linear layer, so the finite difference is taken through a function whose output is bounded in (0, 1) and whose gradient is correspondingly small; the difference quotient loses digits to cancellation before any derivative is formed. It sits below the 1e-7 tolerance with room, and the tolerance is uniform rather than tuned per case.

One case carries a deliberately loosened tolerance, composite/long-cumprod at 1e-5, and the reason is stated in the source: a twelve-element cumulative product spans three orders of magnitude, so the forward pass is ill-conditioned before differentiation begins. It is loosened rather than removed, and the loosening is visible.

What this found

One real defect, and it is the headline of docs/BUGS.md: QLinear and QLinear4 returned tensors with no autodiff graph behind them, so grad through a quantised linear layer answered zero for every upstream parameter while still returning the right value. Fixed in 5344302.

It is worth being precise about why exhaustiveness rather than representativeness found it. The two quantised kernels were the least-exercised operators in the package. A gradient check over the operators someone thought to check would never have reached them, and the defect they had was the worst in the package: not a wrong number, but a plausible one.

What this does not check

Finite differences validate the derivative of the function the interpreter actually computes. If a forward kernel is wrong, the gradient check will happily confirm that its derivative is computed correctly. Forward correctness rests elsewhere: on the golden corpus, on the differential comparison against the self-hosted implementation, and on the closed forms the examples are measured against, such as the Black-Scholes price, delta and vega that examples/montecarlo_option.tw reproduces to four figures.

2. Shape checker soundness

The claim, stated precisely

The checker makes one claim and explicitly declines the other.

It claims: every diagnostic it reports is a real mistake. No false positives.

It does not claim: that a clean check means the program runs. The package comment says it "reports a diagnostic only when a mismatch is certain" and docs/design.md calls the bias toward precision over recall deliberate.

These are not two halves of one property, and conflating them is how a correctness section ends up asserting something untrue. What follows tests the first and measures the second. I am not going to argue that the checker is sound in the sense of accepting only correct programs, because it is not, and the counterexample is six lines.

The checker accepts programs that fail at runtime

let n = len([1.0, 2.0, 3.0])
let A = zeros(2, n)
let x = zeros(2)
let y = A @ x
print(y)

$ twill check unsound.tw
unsound.tw: no shape problems found

$ twill run unsound.tw
unsound.tw:4: runtime error: shape mismatch in @: [2 3] @ [2] (inner 3 != 2)
  4 | let y = A @ x

The mechanism is exactly the design. The checker cannot fold len([1.0, 2.0, 3.0]) to 3, so n types as Unknown, so zeros(2, n) types as Unknown, and an Unknown operand makes the @ undecidable. It stays silent, as designed, and the mismatch reaches the runtime.

This is not an obscure corner. Any shape derived from data read at runtime, from read_csv, from a length, or from a loop-carried value has the same property, and those are ordinary things for a program to do.

There is a second entrance to the same gap that has nothing to do with runtime data, and it is worth naming because it is easy to walk into: grad is a shape barrier. A lambda applied directly is checked. The identical lambda wrapped in grad is not.

let h = fn(v) = sum(zeros(2, 3) @ v)
print(h(zeros(2)))

$ twill check direct.tw
direct.tw:1: shape error: shape mismatch in @: [2, 3] @ [2] (inner 3 != 2)
  1 | let h = fn(v) = sum(zeros(2, 3) @ v)

let g = grad(fn(v) = sum(zeros(2, 3) @ v))
print(g(zeros(2)))

$ twill check viagrad.tw
viagrad.tw: no shape problems found

$ twill run viagrad.tw
viagrad.tw:1: runtime error: shape mismatch in @: [2 3] @ [2] (inner 3 != 2)
  1 | let g = grad(fn(v) = sum(zeros(2, 3) @ v))

Same body, same argument, same mistake; the only difference is grad. In the first program the checker pushes the applied argument's [2] into v and decides the @. In the second, grad returns a function whose parameter shape the checker does not relate to the shape of the lambda it was given, so v types as Unknown and the @ becomes undecidable.

This is the same Unknown-propagation mechanism as above rather than a new one, but it lands in the place twill most advertises, which makes it the version worth knowing. It is a completeness gap and not a soundness one: the checker still says nothing false. Relating grad(f)'s parameter to f's would close it and is a bounded change, since grad preserves the shape of the argument it differentiates with respect to.

Annotating the lambda parameter does not close it either, because the argument that goes wrong is supplied at the application of g, not inside the body.

The claim it does make, tested against the interpreter

Testing "no false positives" on hand-written examples proves little, since the examples are written by the same person who wrote the rules. So it is tested differentially against the interpreter over generated programs.

internal/checker/soundness_test.go generates programs from a small grammar: matmuls, matrix-vector products, elementwise combinations with and without broadcasting, reshapes, concats, calls to shape-annotated functions, and chains where a mismatch is several operations from its cause. Every dimension is a literal drawn from {1, 2, 3, 4}, so the checker has everything it needs to decide, roughly half the programs are broken, and 1 is in the set because it broadcasts against anything and is the case a naive equality rule gets wrong. The seed is fixed, so a disagreement found once can be found again.

Each program is both checked and run, and the two outcomes are treated asymmetrically:

• Checker reports a diagnostic and the program runs. A false positive. Breaks the claim. Fails the test.
• Checker is silent and the program fails at runtime. A false negative. Permitted by design. Counted and reported, so the number is visible rather than merely admitted to.

Result over 4,000 generated programs:

Zero false positives. The claim the checker makes holds over 4,000 programs it did not see while it was being written.

And the completeness it declines to claim, measured

Because every generated program has literal dimensions throughout, a shape error in one is statically decidable in principle. So the same corpus measures what fraction the checker actually decides, which turns "best-effort" from an adjective into a number.

Of 2,646 statically decidable shape errors, the checker caught 2,646, or 100%.

TestCheckerCatchesWhatItCanSee asserts a 95% floor rather than the exact figure, so improving the checker does not break the test and regressing it does.

Reading that honestly

100% on this corpus is a real result and a bounded one. It says that where shapes are statically knowable the checker does not miss, and the grammar covers the operations a numeric program is mostly made of. It does not say the checker is complete, because the corpus is by construction the decidable case. The gap between the two is exactly the example at the top of this section, and it is not narrowing: it is where the design put it.

The corpus is also small in another way. A generated program is at most five lines. It does not exercise nested closures, records, loops that reshape, or grad, all of which the checker leaves Unknown. Extending the generator is the obvious next step and would lower the 100%, which is the point of measuring it.

The other evidence

TestExamplesRunClean in internal/interp/examples_test.go shape-checks and runs every program in examples/, asserting zero diagnostics and a clean run. That is the no-false-positive property on 23 real programs rather than generated ones, and it has been in the suite since before this document.

3. What is verified, in one place

The self-hosted row, in full

The two rows above used to be one, and it read "Forward numerics match the self-hosted implementation | the differential harness, tools/diff/ | 443 files on check, 89 on fmt". Three things were wrong with it. The evidence named, tools/diff/, takes -old and -new Go binaries and never looks at src/, so it cannot have produced that result. Nothing in the Makefile or .github/workflows/ci.yml runs it in any case. And the property claimed, forward numerics, was being supported by counts from check and fmt, which are front-end stages and say nothing about numerics.

A fourth thing was wrong with the first attempt to replace it, and it is worth recording because it is the same failure in a smaller size. That version named testdata/cases, examples, std and src and gave a count that was those four names read as top-level globs, so everything in their subdirectories was left out of the number while the sentence claimed the tree. A coverage number that overstates its own evidence is exactly what this section exists to stop, which is why the rows above now carry no count at all: the corpus grows, and the claim is about every file in it.

What is true, measured 2026-09-04 by running ./twill <cmd> f against ./twill run src/main.tw <cmd> f over every .tw file git ls-files '*.tw' reports, which is the whole tree read recursively:

• check agrees on every file, exit status for exit status, src/eval.tw included. It is not fast: some files take minutes through the self-hosted checker against well under a second on the bootstrap, so a harness with a per-file cap in the tens of seconds reports them as timeouts rather than as agreement.
• fmt agrees on every file once blank lines are set aside. Most are byte-identical; the rest differ only in the by-design rule where the self-hosted printer keeps blank lines the Go printer drops, in every one of them the extra lines are the self-hosted side's, and no token differs anywhere.
• The evaluator does not agree. A large minority of the names in src/builtins.tw reach "named in the builtin table but has no implementation"; docs/BUGS.md entry 12 and its Open section carry the current split and the probe that re-derives it. Beyond the refusals there are wrong answers: examples/gbm.tw exits 0 on both sides with a test regression RMSE of 0.660285 against 0.659657, a fourth-decimal disagreement and not the 1-ULP kind section 4 is about.

docs/roadmap.md, "What the second implementation agrees on, and what it does not", carries the detail and the reproductions.

4. What "reproduces exactly" does not cover: another architecture

Measured on 2026-09-01, arm64 (Apple silicon) against linux/amd64 in a container, the same commit built by the same Go version:

f64_exp(0.37)   arm64  0x1.729ebc574421cp+00
                amd64  0x1.729ebc574421dp+00

One ULP, and it is not twill's arithmetic. math.Exp in the Go standard library has an architecture-specific implementation, and the two do not agree in the last bit. Nothing in this repository can make them agree; twill's own operations would have to stop using the platform's exp to do it.

Two of the three differences that turned up in that comparison were twill's, and both are fixed. A gradient accumulation written g += d * cotangent contracted into a fused multiply-add on arm64 and not on amd64, and FormatNumber decided whether a float was whole with a conversion that is undefined out of range. What remains, after those, is exp and the operations built on it.

Matrix multiply had the same fused-multiply-add divergence, and it is now the default that avoids it. The comparison above did not catch it because every matmul test compared with a tolerance and none pinned bits, so the arm64 kernel quietly fused its inner product while amd64 did not. As of 1.15.0 the default matmul kernel rounds every product before adding it, so it is bit-identical across architectures, pinned by TestStrictMatMulIsBitIdentical. The faster TWILL_MATMUL=fast kernel reintroduces the fused multiply-add on purpose and is not bit-identical across architectures; it is opt-in for exactly that reason. As of 1.16.0 the fast path also runs a hand-written, register-blocked and packed microkernel for both f64 and f32, several times faster than the earlier fast kernel on the large sizes: on arm64 using NEON, as of 1.17.0 on amd64 using AVX2 with FMA3, and as of 1.18.0 on amd64 using AVX-512 when the CPU has it. Selection is a runtime fallback chain: AVX-512 if present, else AVX2 with FMA, else the pure-Go reference. It fuses through FMA and reorders the summation, so it is within tolerance of strict and not bit-identical, and a fast result may also differ between arm64 and amd64 since the two fuse in a different order. The strict default is unchanged. The amd64 AVX2 kernel is validated for correctness on the linux/amd64 CI job, not on the arm64 development machine. The amd64 AVX-512 kernel is compiled and vetted and the tolerance and fuzz tests exercise it on any machine that has AVX-512; whether that happened on CI is recorded in the CI log, since a GitHub-hosted runner may not expose AVX-512, in which case the AVX-512 path is compiled and vetted but not executed. docs/BENCHMARKS.md sections 10, 11, 12 and 13 have the numbers.

Why one bit matters here and usually does not. A single tensor operation is off by an ULP and nobody can tell. An iterative method that feeds its own output back in is a different case: twill-lang/heddle's NUTS test samples a half-normal posterior with a fixed seed, 500 warmup and 4,000 draws, and asks that the mean come back within 0.03 of sqrt(2/pi). It passes on amd64 at 27/27 and fails on arm64 by 0.032 — one trajectory diverges early, the sampler takes a different path, and the answer moves by a thousand times the input difference. That is the algorithm behaving correctly. It is what a seeded sampler does with any perturbation.

So the README's "a program reproduces exactly" is a claim about one machine. Across two machines of the same architecture it holds; across architectures it holds for everything that does not go through a libm function, and for anything that does, it holds to the precision the method itself preserves. A test that pins a number produced by an iterative float method is a test that pins the architecture it was written on, and should say so.

The gate, and why it is the whole of CI

make check runs what CI runs: build, gofmt, vet, the full test suite, and the race pass with CI's own flags and timeout. make ci adds the two linters, which are separate only because they fetch a tool and need the network.

This is written down because the gate was wrong once and it cost a release. check was vet test plus a gofmt check, and was commented "What CI runs", which it had stopped being: CI also ran go test -race -short -timeout 25m and a lint job. 1.6.5 was tagged on a green local run and its CI failed, because the test suite had grown past the race pass's budget and nothing local was measuring that.

The failure was a timeout rather than a data race, and the cause is worth knowing for anyone adding to the corpus: two of the examples train a small model and take fifteen seconds each where every other example is milliseconds, and the corpus is walked twice -- once as written, once as formatted. Under the race detector that was most of the budget. Those two, and the self-hosted differential runs, are skipped when -short is passed, which is the flag the race pass uses and the only pass that uses it. The ordinary run has no -short and runs all of them on every build.

So: a new example that trains anything belongs in heavyExamples, and a new test that spawns the self-hosted compiler belongs behind skipUnderShort. Neither reduces what is checked; both keep the race pass measuring what it is for, which is the parallel tensor kernels rather than a tree walk over a twill source file.