Version 0.4 (draft). Status: design complete for a v1 compiler; open items listed in section 15. Changes from 0.1 are recorded in Appendix B, from 0.2 in Appendix C, and from 0.3 in Appendix D.
Prova is a programming language designed for code generation by large language models. Its founding principle:
A Prova program is a claim plus its evidence. The compiler rejects claims without evidence.
Every design decision in this document is subordinate to that principle and to four consequences of how LLMs fail: they hallucinate plausible interfaces, they lose distant context, they generate without backtracking, and they improve through tight generate-check-repair loops. Prova therefore optimises for checkability over writability, locality over expressiveness, and structural manipulation over textual manipulation.
Non-goals for v1: human ergonomics beyond readability, metaprogramming, typeclasses or traits, inheritance, exceptions, implicit conversions, concurrency primitives (see 15).
Prova is a target, not a representation. It occupies the position a general-purpose programming language occupies, at the altitude of code, and its claim is not that this altitude is wrong but that the guarantees usually available at it are too weak for a generated artefact to be trusted.
This distinguishes Prova from the parallel line of work in which a higher-level representation of a domain, expressed as entities, states, transitions and permissions, becomes the source of truth, and code, tests, interfaces and deployment are all derived artefacts regenerated from it. That approach holds that code is the wrong level of description for a model to work at. Prova holds that code is the right level and that the problem is the absence of evidence.
The two positions compose rather than compete, and Prova is designed to be composed with. A representation of that kind must eventually produce a program, and a representation that produces Prova yields a program whose claims are proved, whose effects are declared, whose termination is guaranteed and whose examples execute at compile time. Prova is intended to be a worthwhile thing to generate, whether the generator is a model working directly, a higher-level representation, or a person.
Prova therefore defines no natural-language surface, no domain-description layer above the language, and no mechanism for deriving one language from another. Anything of that kind belongs above Prova and outside this specification.
Prova source is UTF-8 text composed of s-expressions.
Tokens: parentheses ( ), atoms, and string literals. Atoms are symbols, integers, decimals, booleans (true, false), and the wildcard _. Symbols match [a-z][a-z0-9-]*[?!]? for values and functions, [A-Z][A-Za-z0-9]* for types, constructors and capabilities. Comments begin with ; and run to end of line. Comments are preserved as attachments to the following node in the syntax tree.
There is exactly one canonical formatting, defined by the reference formatter prova fmt, which takes no options. All conforming tools emit canonical form. Two programs are textually identical if and only if their syntax trees are identical. A compiler MUST reject no program on formatting grounds but MUST offer canonicalisation; CI configurations are expected to require canonical form.
Literals denote values, not spellings. A numeric literal is parsed to the value it denotes and the syntax tree records that value; the digits as typed are not retained and no operation may recover them. 42 and 00042 are therefore the same program with the same tree, -0 is the integer zero, and canonical form is one form per value rather than one form per spelling. This is the same rule that governs Decimal identity in 4.1 and holds for the same reason: two programs denoting the same value must not be distinguishable by any pure function, or equality ceases to be a congruence and the encoding of 6.1 is unsound. It also follows from the purpose of canonical form, since a spelling that survives into the tree is a difference the language would carry for no gain.
Consistent with 2's rule that a compiler must reject no program on formatting grounds but must offer canonicalisation, a non-canonical spelling of a well-formed literal is not an error. It parses, and it renders canonically.
Identifier policy: the formatter and linter enforce no abbreviations from a stop-list (cnt, idx, tmp, mgr, and so on, list maintained in the toolchain). Names are descriptive by convention and this is treated as a lint error, not a style suggestion, because identifiers carry semantic signal for model and prover alike.
EBNF, where * is zero or more, + is one or more, ? is optional.
program ::= form*
form ::= module | defn | defspec | deftype | defcap | expr
module ::= "(" "module" name needs provides form* ")"
needs ::= "(" "needs" capparam* ")"
capparam ::= "(" name captype ")"
provides ::= "(" "provides" providesig+ ")"
providesig ::= "(" name signature ")"
defn ::= "(" "defn" name signature contract? measure? examples body ")"
defspec ::= "(" "defspec" name specsig examples body ")"
deftype ::= "(" "deftype" TypeName typedef ")"
defcap ::= "(" "defcap" CapName opsig+ ")"
opsig ::= "(" name signature ")"
signature ::= "(" "sig" "(" param* ")" "->" type "!" effects ")"
specsig ::= "(" "sig" "(" param* ")" "->" type "!" "pure" ")"
param ::= "(" name type ")"
effects ::= "pure" | "(" name+ ")"
contract ::= requires? ensures?
requires ::= "(" "requires" specexpr+ ")"
ensures ::= "(" "ensures" specexpr+ ")"
measure ::= "(" "decreases" specexpr ")"
examples ::= "(" "examples" example+ ")"
example ::= "(" "example" expr "=>" expr ")"
typedef ::= record | union | refine | alias
record ::= "(" "record" field+ ")"
field ::= "(" name type ")"
union ::= "(" "union" variant+ ")"
variant ::= "(" TypeName field* ")"
refine ::= "(" "refine" type specexpr ")"
alias ::= type
type ::= TypeName | "(" TypeName type+ ")"
body ::= expr
expr ::= atom
| "(" expr expr* ")"
| "(" "let" "(" binding+ ")" expr ")"
| "(" "if" expr expr expr ")"
| "(" "match" expr clause+ ")"
| "(" "trust" string trustable ")"
binding ::= "(" name expr ")"
clause ::= "(" pattern expr ")"
pattern ::= "_" | literal | name | "(" TypeName pattern* ")"
trustable ::= ensures | expr
specexpr ::= (expr restricted to the specification fragment, see 6.1)
Notes. defn without a contract carries the trivial contract (requires true, ensures true); the examples block is never optional. measure is required whenever recursion is not structural (see 8). trust is defined in 6.4.
Unit, Bool, Int (arbitrary precision), Nat (defined as (refine Int (>= _ 0))), Decimal (exact decimal arithmetic; there is no binary floating point in v1), Text (immutable UTF-8), Bytes.
The identity of a Decimal is numeric: the values written 150 and 150.00 are the same value, trailing zeros are not observable, and no operation may reveal the precision at which a value was written or computed. A Decimal therefore carries no precision of its own, and rendering one as Text takes the number of decimal places as an explicit argument (14), as rounding does (9). Equality on Decimal is consequently a congruence: no pure function distinguishes equal values, which is what permits the encoding of 6.1.
Value representation is an implementation matter, constrained only by the rules above. Exact decimal arithmetic is long-established and an implementation is expected to follow proven practice rather than devise anything: results are exact, arithmetic never silently rounds, and there is no binary floating point at any stage.
The two constraints intersect and the reconciliation is deliberate. Established practice records a scale alongside the digits, and an implementation may do exactly that; what it may not do is expose it. The rules above are semantic and bind the language surface, not the storage: no operation of the language, and no rendering of a value by any tool, may distinguish two decimals that are numerically equal. An implementation that records a scale internally therefore either normalises before any observable operation or omits the precision-exposing operations of the practice it borrows from. Both are conforming; exposing the scale is not.
(List T), (NonEmptyList T), (Option T) with constructors Some and None, (Result T E) with constructors Ok and Err, (Map K V) where K admits equality, (Set T).
Records and unions per the grammar. Construction uses the type or variant name in application position: (Order id lines total), (Placed at). Field access is (.field record). Functional update is (with record (field value)+). There is no inheritance and no subtyping between named types; refinement subtyping (4.4) is the only subtyping in the language.
(refine T p) denotes the values of T satisfying predicate p, where p is a specexpr over the hole _. Refinements are subtypes of their base: any (refine T p) may be used where T is expected. The reverse direction generates a proof obligation. Where the obligation cannot be discharged from context, the program must narrow explicitly:
(match (check NonZero d)
((Some nz) (divide n nz))
(None (Err DivisionByZero)))check is the built-in refinement witness: (check R x) has type (Option R) where R is a refinement of the type of x. Its cost is one predicate evaluation.
Refinements compose through the program by flow: the verifier propagates known facts along control flow (a match arm knows its pattern held, an if branch knows its condition) so obligations arise only where knowledge genuinely runs out.
Every signature carries an effect row: pure or a set of capability parameter names drawn from the enclosing scope. Effects are not inferred; they are declared, and the compiler checks the body against the declaration in both directions. A body performing an operation of a capability not in the row is an error; a row naming a capability the body never uses is a lint error (dead effect).
A capability type is declared with defcap as a set of operation signatures:
(defcap ClockCap
(now (sig () -> Timestamp ! (self))))Capabilities are ordinary values. They cannot be constructed in user code; they are introduced only by the runtime at the program root and by attenuation (a library function may wrap a capability in a narrower one). Purity is the empty row: a pure function is deterministic, total (guaranteed by 8), and free to be memoised, reordered or evaluated at compile time.
The single form for defining a runtime function, in fixed order: name, signature, contract, measure where required, examples, body. All parts are checked; none is documentation.
Specification-level functions, usable in contracts and refinements. Restrictions: pure effect row, specexpr body (6.1), structural recursion only, totality enforced. Spec functions are compiled twice: once to executable code (they are callable at runtime like any pure function) and once to logic for the prover.
Per the grammar. Type recursion is permitted for unions (enabling inductive data); records may not be directly self-referential except through a union or a built-in constructor.
A module names its capability needs and its provided signatures. Everything not listed in provides is private. Imports do not exist as a textual construct; a module refers to provided names of modules it is linked against, and linking is performed by the toolchain against the needs/provides graph. Consequences the compiler MUST enforce: no module accesses any capability not in its needs; the capability graph of a program is statically known; a module with empty needs is certified inert and marked as such in build metadata.
Specexprs are the sublanguage of expressions permitted in requires, ensures, refinements, measures and spec bodies. It contains: literals; parameters and result (in ensures only); let, if, match; applications of spec functions and of the built-in pure operators on base types (arithmetic, comparison, boolean connectives, equality, constructors, field access, and the built-in list and map observers length, member?, nth, keys); and quantifiers (forall ((x T)) p) and (exists ((x T)) p) where T is finitely enumerable from context or the quantifier is over the elements of a concrete collection in scope. General recursion, capabilities and trust are excluded.
The fragment is designed to translate to SMT-LIB 2 over the theories of linear integer arithmetic, real arithmetic including nonlinear multiplication, algebraic datatypes, uninterpreted functions and arrays. Decimal is modelled as a real. That encoding is sound in the proving direction, because every Decimal is a real and a property proved of all reals holds of all decimals; it is not sound in the refuting direction, and 6.3 governs the consequence. A conforming compiler MUST implement the translation and MAY use any SMT solver; the reference implementation targets Z3 with CVC5 as cross-check.
The verifier emits an obligation at each of the following points: a call site, that the callee's requires holds; a function body, that ensures holds on every return path given requires; a refinement coercion, that the predicate holds; a measure, that it is a Nat and strictly decreases at every recursive call; a match, that patterns are exhaustive (discharged syntactically where possible, by the solver where refinements narrow the space); an example, that its input satisfies requires and its asserted output satisfies ensures.
Each obligation resolves to exactly one of three outcomes.
Proved: the solver establishes validity. Silent success.
Disproved: the solver produces a model violating the obligation. The compiler MUST report the counterexample as structured data: obligation identity, tree location, and concrete values for all free variables. The toolchain offers a one-step action converting a counterexample into a failing example in the relevant examples block.
Where a model assigns a real value to a variable of type Decimal (6.1), the compiler MUST establish that the value is representable as a finite decimal before reporting it. A witness that is not so representable, one third being the standard case, does not disprove the obligation and MUST NOT be reported as a counterexample.
Suppressing such a witness does not settle the obligation, because a representable counterexample may exist even though the solver returned an unrepresentable one. Before resolving the obligation as Unknown on this path, the compiler MUST issue at least one further query constraining the Decimal-typed free variables to representable values, and MUST report a counterexample if that query produces one. Only if the further query is itself inconclusive does the obligation resolve as Unknown, and the diagnostic on this path MUST state that an unrepresentable counterexample was found and that representable ones were not ruled out. An author reaching for trust (6.4) in the face of such an Unknown is entitled to know that the solver found a violation and that only its representability was in doubt.
Unknown: timeout or fragment escape. Unknown is a compile error unless the obligation is wrapped in trust. The default per-obligation solver budget is 10 seconds, configurable per project, never per file.
Nonlinear real arithmetic (6.1) is decidable but expensive, and a fixed budget will therefore yield Unknown more often than the linear fragment would, on precisely the arithmetic Decimal exists to serve. This is the price of admitting obligations that 0.1 could not express at all, but it creates pressure to raise the trust budget (6.4) above its default of zero merely to keep a project compiling, which would trade proof for justification at scale. A conforming implementation MUST therefore report, in build metadata, how many obligations resolved Unknown and how many of those took the unrepresentable-witness path above, so that the pressure is visible as a number rather than felt as friction.
(trust "justification" obligation-or-expr) demotes the enclosed obligations from static proof to runtime check plus mandatory adversarial testing (see 10). Rules: the justification string is required and must be non-empty; trust is not permitted in defspec; every runtime violation of a trusted obligation raises a contract fault, which terminates the program's current capability scope (there are no catchable exceptions; a fault is an orderly abort with a structured report); prova audit lists every trust with its justification, and projects declare a maximum trust count in build configuration, which the compiler enforces. The default maximum is zero.
Debug builds additionally evaluate all requires and ensures at runtime even when proved, as a soundness check on the compiler itself. Release builds erase proved contracts entirely and retain only trusted checks. Erasure is sound because proofs are machine-checked; the compiler MUST record in build metadata which obligations were erased and under which solver versions they were proved.
The examples block is executable specification. Semantics: each example's left expression is evaluated in a pure context at compile time (examples may not use capabilities; a function whose effect row is non-pure gives examples against a compiler-synthesised capability stub that records and replays declared interactions, defined in the toolchain specification); the result must equal the right expression under the equality of 9; each example is additionally checked against the contract per 6.2. A defn or defspec with zero examples does not compile. Examples are the training corpus the language carries within itself: tools and models treat them as the primary demonstration of intent.
All Prova functions are total. Recursion is admitted in two forms: structural, where some parameter descends strictly through constructors of an inductive type on every recursive call, verified syntactically; or measured, where the declared decreases expression is proved a strictly decreasing Nat. Mutual recursion requires a single shared measure across the group. Non-terminating computation is inexpressible; long-running programs are structured as event loops provided by the runtime, where each event handler is total.
Evaluation is strict, left to right, innermost first. All values are immutable. Mutation is available only through StateCap operations, so every function that can observe or effect state change says so in its row. Errors are values: Option and Result are the only error mechanisms, there are no exceptions, and the sole abnormal path is the contract fault of 6.4, which is not catchable. Equality is structural on all types except capabilities, which admit no equality, and Decimal, whose equality is numeric per 4.1. Integer arithmetic never overflows (Int is unbounded); division and modulo require NonZero divisors by their built-in signatures, so division by zero is a compile-time impossibility outside trust. Division on Decimal is exact: it carries a proof obligation that the quotient is finitely representable as a Decimal, so an inexact division does not compile. Rounding is never implicit. A computation that requires rounding uses the prelude's rounding division (14), which states precision and rounding mode explicitly and is total.
The toolchain derives generators automatically from types: base types have built-in generators, algebraic types compose them, refinements are generated by constrained generation with solver assistance (the solver enumerates satisfying models) falling back to generate-and-filter. Shrinking is structural and preserves refinements.
Mandatory application: every trust block is exercised by generated inputs at verification time, default 10,000 cases per obligation, shrunk on failure to a minimal counterexample reported in the same structured format as 6.3. A generated counterexample is a compile error exactly as a disproof is. Optional application: prova hammer runs generation against all proved obligations as a compiler-soundness audit; conforming implementations must provide it, projects choose when to run it.
The compiler is a service before it is a command. A conforming implementation MUST expose the following as structured (JSON) request-response operations, and the CLI MUST be a thin client of the same interface.
parse text to tree and diagnostics. format tree to canonical text. check tree to typed tree and diagnostics. verify typed tree to obligation results per 6.3, each carrying a stable obligation identifier, tree path, status, counterexample where applicable, and where feasible a repair suggestion expressed as a tree edit. edit applies structural operations addressed by tree path: replace-node, insert-form, delete-form, rename-symbol (project-wide, semantics-aware), add-example. test runs examples and property generation with structured results. audit reports the trust ledger and the capability graph. build compiles a program to an executable artefact per 12 and reports diagnostics and build metadata. explain renders any diagnostic, obligation or counterexample as prose for human review.
The toolchain has no ambient authority over the filesystem, for the same reason a program does not (13). build writes only within a project-relative output location: a request MUST NOT name a destination outside it, a destination that resolves outside it after path traversal MUST be rejected as a diagnostic rather than followed, and overwriting an existing artefact MUST be reported as a diagnostic rather than performed silently. A compiler that enforces the absence of ambient authority in the programs it compiles, while exercising it itself, does not deserve to be believed about the programs.
Every diagnostic in every operation carries: a stable code, a tree path (never only a line number), the relevant obligation or rule, and machine-readable data sufficient to act without parsing prose. Prose renderings exist for humans and are never the primary representation.
A conforming compiler processes each module through: parse and canonicalise; name and capability resolution against the module graph; type checking with refinement subtyping; effect checking; totality checking; obligation generation; solving with per-obligation budget; trusted-obligation instrumentation and property testing; example execution; code generation. A module compiles if and only if every stage succeeds and every obligation is proved or trusted within the project's trust budget. The reference backend targets native code via compilation to Go in v1 (chosen for runtime simplicity and deployment convenience; the language semantics do not depend on the backend).
The v1 compiler is itself written in Go. Host language and backend target are independent choices, and neither is a property of the language. From v1 onward, subsequent versions of the compiler are written in Prova and built by the preceding compiler. The v1 Go compiler is retained as a permanent, versioned, reproducible bootstrap seed and is not discarded once self-hosting is reached. A compiler written in Prova is subject to Prova's own rules, including mandatory examples (7), totality (8) and the default trust budget of zero (6.4).
A program declares a root module whose needs are its complete authority. The runtime constructs exactly the requested root capabilities and invokes main with them:
(module app
(needs (fs FsCap) (http HttpCap) (clock ClockCap))
(provides (main (sig () -> Unit ! (fs http clock))))
...)Nothing else is ambient. Standard capabilities defined by the runtime specification: FsCap, HttpCap, ClockCap, RandomCap, EnvCap, StateCap, SpawnCap (reserved for the future concurrency design). Attenuation combinators in the standard library produce narrowed capabilities (read-only filesystem rooted at a path, HTTP restricted to a host allow-list) so that least authority is cheap to express.
The prelude is deliberately small and every function in it carries full contracts and examples, serving as the exemplar corpus. Contents: constructors and observers for the built-in types; total list operations (map, filter, fold, append, reverse, sort with a proved permutation-and-ordered contract); text operations; Result and Option combinators (map-ok, and-then, unwrap-or); comparison and arithmetic; the rounding division on Decimal required by 9, which takes an explicit precision and rounding mode and is total; the rendering of a Decimal as Text required by 4.1, which likewise takes an explicit number of decimal places and rounding mode, so that a monetary amount is printed to two places by asking for two places rather than by relying on the value to remember them; check per 4.4. Nothing in the prelude requires capabilities.
Concurrency (structured, capability-scoped, likely session-typed channels; SpawnCap is reserved). A typeclass-like mechanism only if evidence shows the duplication cost exceeds the ambiguity cost for generation. Proof-carrying compiled artefacts, so binaries ship their discharged obligations. Gradual interop with host-language libraries through capability-wrapped foreign interfaces, which necessarily enter as trust.
(module pricing
(needs)
(provides
(apply-discount (sig ((total Money) (d Discount)) -> Money ! pure))))
(deftype Money (refine Decimal (>= _ 0)))
(deftype Percent (refine Decimal (and (>= _ 0) (<= _ 100))))
(deftype Discount
(union (NoDiscount)
(PercentOff (p Percent))
(AmountOff (a Money))))
(defspec discounted-not-larger
(sig ((before Money) (after Money)) -> Bool ! pure)
(examples
(example (discounted-not-larger 100 90) => true)
(example (discounted-not-larger 100 100) => true)
(example (discounted-not-larger 100 101) => false))
(<= after before))
(defn apply-discount
(sig ((total Money) (d Discount)) -> Money ! pure)
(ensures (discounted-not-larger total result))
(examples
(example (apply-discount 200 (NoDiscount)) => 200)
(example (apply-discount 200 (PercentOff 25)) => 150)
(example (apply-discount 200 (AmountOff 300)) => 0))
(match d
((NoDiscount) total)
((PercentOff p) (* total (/ (- 100 p) 100)))
((AmountOff a) (match (check Money (- total a))
((Some m) m)
(None 0)))))Every claim above is proved: the percentage branch stays within Money because p is a Percent, the amount branch narrows explicitly, the postcondition is discharged for all three constructors, exhaustiveness is syntactic, and the examples bind the semantics concretely. This is the shape of all Prova code: claim, evidence, and nowhere to hide.
Three points in this example depend on decisions made in 0.2 and are worth naming, because under 0.1 the module did not compile. The second example asserts 150 against a computed quotient and product, which holds because Decimal identity is numeric (4.1) rather than sensitive to trailing zeros. The division by 100 is admitted because it is exact, as 9 requires. The postcondition on the PercentOff branch multiplies two variables and is therefore nonlinear; it is dischargeable because 6.1 models Decimal as a real and admits nonlinear real arithmetic, which the theory list of 0.1 did not.
Three decisions resolve questions on which 0.1 was silent or self-contradictory, all concerning Decimal. Two further items record implementation commitments that 0.1 did not address.
-
Decimalidentity is numeric (4.1, and the carve-out in 9). 0.1 stated that equality is structural on all types except capabilities, and did not fix what makes two decimals identical. Under a representation that records precision,150and150.00would have been distinct, and Appendix A's second example would have failed under 7. Identity is now numeric and precision is not observable. Value representation remains an implementation matter, to be settled by established practice rather than invention.This is the one point where Prova departs from the mainstream decimal types, and the departure is deliberate. IEEE 754-2008, Python and C# all agree with Prova that comparison is numeric, but all of them keep the precision inside the value and let a program observe it, through quantum propagation and through formatting. Java goes further still and makes
equalssensitive to it, which is the behaviour Prova's 7 could not tolerate. Prova instead discards precision from the value and takes it as an argument where it is needed, in rounding (9) and in rendering (14). The reason is 6.1: a language that proves its claims needs equality to be a congruence, so that equals may be substituted for equals, and a formatting function able to tell150from150.00would break exactly that. Mainstream decimal types carry no proof obligations and so never had to choose. -
Division on
Decimalis exact (9, 14). 0.1 required aNonZerodivisor, making division by zero impossible at compile time, but was silent on inexactness, and no finite decimal represents one third. Division now carries a proof obligation of finite representability, and rounding is available only through an explicit prelude operation stating precision and mode. -
Decimalis modelled as a real and the fragment admits nonlinear real arithmetic (6.1, with the counterexample rule in 6.3). The theory list of 0.1 was linear integer arithmetic, algebraic datatypes, uninterpreted functions and arrays.Decimalwas absent from it, and Appendix A's postcondition is nonlinear, so under 0.1 combined with the rule in 6.3 that fragment escape is a compile error, the worked example's own obligation was not dischargeable. Because the encoding is unsound in the refuting direction, 6.3 now requires that a counterexample be checked for decimal representability before it is reported. -
The v1 compiler is written in Go (12). 0.1 fixed Go as the compilation target and said nothing about the implementation language of the compiler. The two are independent, and neither is a property of the language.
-
The toolchain is to become self-hosting (12). From v1 onward, compilers are written in Prova and built by the preceding compiler, with the v1 Go compiler retained as a permanent bootstrap seed. 0.1 did not address this, and it does not appear in the deferred list of 15.
Two changes. One states a position the specification had always implied without asserting; the other closes a gap found by security review of 0.2 before any of it was implemented.
-
Prova's position is stated: it is a target, not a representation (1.1). 0.2 described what Prova is and how it behaves but never said where it sits relative to the approach in which a higher-level domain representation is the source of truth and code is a derived artefact. The omission left the question to be answered by inference, and inference could go either way. Prova takes the position that code is the right level of description and that the deficiency is the absence of evidence, not the altitude. It defines no natural-language surface and no domain-description layer, and it is designed to be a worthwhile thing for such a layer to generate. Nothing else in the document changes as a consequence; 1.1 records a decision already embodied throughout.
-
A suppressed counterexample no longer ends the enquiry (6.3, with a metadata requirement in the Unknown clause of the same section). 0.2 required that a counterexample assigning an unrepresentable real to a
Decimalbe discarded, which is correct, but then let the obligation fall to Unknown without asking whether a representable counterexample existed. It did not, and the defect was demonstrable: a false claim about decimals yielded the witness one sixth, which 0.2 required be discarded, while the same query constrained to two decimal places yielded one hundredth immediately, an ordinary decimal and a genuine disproof. The rule as written threw away evidence that existed, which is the precise inverse of the founding principle. 0.3 requires a further query constrained to representable values before Unknown may be returned, and requires the resulting diagnostic to disclose what was found and what was not ruled out.The same section now also requires build metadata to report the Unknown count and the share of it taking the unrepresentable-witness path. Nonlinear real arithmetic costs more than the fragment of 0.1 and will time out more often on exactly the arithmetic
Decimalserves; without a number, that pressure is felt as friction and relieved by raising the trust budget, which trades proof for justification quietly and at scale.
Two changes. Both close silences rather than revise decisions, and both were found by implementation reaching a point the specification had not described.
-
Literals denote values, not spellings (2). 0.3 listed integers among the atoms but never fixed their literal syntax, so leading zeros, a leading sign and negative zero were undefined. An implementation therefore had to choose, and chose to retain the digits as typed, with the result that
42and00042produced different trees and different canonical forms while denoting the same integer. That is the defect 4.1 was amended to prevent forDecimal, arriving by another route: two programs equal in meaning, distinguishable by a pure function, and equality no longer a congruence. Numeric literals now parse to the value they denote and the spelling is not retained. -
buildis specified, and the toolchain has no ambient filesystem authority (11). 0.3 enumerated eight operations in 11 and building was not among them, although 12 sanctions compilation to native code and a compiler plainly must produce artefacts. The operation existed, its shape had never been specified, and it was therefore settled below: a build request naming any absolute path was honoured, path traversal resolved and was followed, and an existing artefact was overwritten in silence. The gap was structural rather than accidental. 13 states that a program has exactly the authority its root module declares and that nothing else is ambient, and 4.5 has the compiler check this in both directions; nothing had ever been said about the authority of the compiler itself.buildnow appears in the operation set, and the toolchain is held to a version of the discipline it enforces.