Combine static assumptions, validation, mutation, and tests into a defensible guarantee.
By the end: identify exactly which obligation belongs to the checker, validator, or application logic.
Inspect the actual chain of evidence
A fictional service parses JSON, asserts User, stores the object, and claims that the type system proves every request has a valid age and belongs to an authorized customer. The declaration describes what later code assumes; the assertion does not establish those assumptions.
Separate syntax parsing, schema validation, authorization, and application invariants. The lab validates only name and age and returns a new small object. It has no account lookup, permission service, concurrency, persistence, or proof that the data is true. Those omissions are boundaries, not hidden successes.
Identify the value and the property each check establishes
A safety claim needs a subject as well as a property. Consider the fictional service's original JSON text, the object produced by parsing it, and the smaller object returned by validation. These are different subjects. Checking the smaller object's age does not approve every field of the parsed object. Authentication means establishing who a sender is. Authorization means deciding what that sender may do. Neither follows from a payload containing a plausible name. To audit the service, attach each conclusion to the value it describes and the operation that supplies its evidence.
JSON parsing checks a representation grammar, the rules for forming JSON text. It distinguishes a properly quoted string from malformed punctuation, but it accepts many structures unrelated to a user record. A number, an array, and an object with an age string can all be valid JSON. Thus syntax success narrows the possibilities without establishing the required schema. A schema is a set of rules for the structure and contents of accepted data. The next operation must inspect the parsed value to establish those rules, rather than relabel syntax success as a user guarantee.
The accepted projection differs from the parsed object
The role field belongs to the input object but not the result. Acceptance does not grant the claimed administrator role.
In this validator, begin by requiring an object that is neither null nor an array. Then require name and age as own fields, meaning fields belonging directly to that object rather than supplied through an inherited lookup. Name must be text, must contain something other than whitespace, and must have at most 30 UTF-16 code units, as measured by JavaScript string length. An ordinary Latin letter uses one unit; many emoji use two, so this is not a visible-symbol count. Age must be a number that is an integer and lies between 0 and 130 inclusive. These requirements are independent. Satisfying the name checks does not excuse a missing age or authorize conversion of age text.
Work through the paper payload {"name":"Mina","age":"20"}. Its punctuation and quoting form valid JSON. The outer value is an object and both required fields exist. Name is nonblank text within the bound. Age, however, is text because the quotation marks are part of the JSON representation of that field. The validator rejects it before treating it as an integer. A type assertion claiming User would not perform any of these inspections. It would merely let later code assume properties that the actual payload has not yet established.
Change the paper age field to the number 20.5. The representation category now passes, but the integer requirement fails. Change it to 131 and the integer requirement passes while the upper bound fails. Change it to 130 and both checks pass. These intermediate cases separate three obligations that an informal phrase such as numeric age often hides. The valid interval is a policy chosen for this schema, not a theorem about human ages or the meaning of the JavaScript number type. A different application could choose a different policy without changing JSON syntax.
Three checks distinguish four plausible age fields
JSON age field
Number?
Integer?
In 0 through 130?
Accepted age?
"20"
No
No
No numeric age
No
20.5
Yes
No
Yes
No
131
Yes
Yes
No
No
130
Yes
Yes
Yes
Yes
All four fields can appear in syntactically valid JSON. Later columns isolate logical requirements, not additional passes after rejection.
After success, the validator constructs a result containing only name and age. For a payload with role set to admin as an extra field, that role does not appear in the result. This is projection, selecting named fields rather than approving or returning the whole input. A service that validates, then stores the original parsed object, has changed the subject of its evidence. The excluded role would be present again. In the local lab there is no storage or account update, so this service scenario is an audit example, not hidden application behavior.
Track changes after validation
If an alias can mutate a validated object, the checked property may no longer hold later. An immutable value, controlled constructor, restricted mutation, or repeated validation may be needed. A mutable Cat cell example shows why a broad writable alias can undermine a narrow claim.
External libraries, unsafe features, assertions, and foreign interfaces are part of the trusted boundary. A sound formal calculus does not prove that a production implementation and all dependencies match its assumptions. Tests and reviews check different parts of that larger chain.
Follow a checked property across copies and aliases
Validation establishes a property at the time of inspection. To use the property later, ask whether the value can change between the check and the use. An alias is another reference to the same object or storage location. If two parts of a program share a writable object, one can change what the other observes. This is not a failure of checking the original value. It is a failure to justify carrying that original conclusion forward after a permitted change. The proof obligation concerns the interval between validation and use.
Imagine a paper service that checks an object whose age is 20 and then gives another component a writable alias. That component writes the text "unknown" into age before the service adds one. The earlier integer check was true, but it no longer describes the current field. This example is outside the lab, which exposes no aliasing or mutation controls. It identifies the missing assumption in a real design. A static type claim that allows only integer writes might preserve the integer property, provided every writer actually obeys that claim and no unchecked boundary bypasses it.
A checked field can change before use
This paper counterexample assumes an unchecked writable alias. The local validator neither offers that write nor certifies arbitrary external mutation.
A stronger schema property needs stronger preservation rules. An age field that remains an integer can still change from 20 to 200. Ordinary integer classification would remain true while this schema's 0 through 130 range would fail. A controlled setter, meaning a function that performs every allowed update, could recheck the range before storing a replacement. Alternatively, a design could prohibit updates and create a newly validated value for each change. These are possible application designs, not implemented features of the validator. The required rule depends on the property being carried forward.
Copying the accepted fields changes the alias argument in this particular lab. The returned object is distinct from the parsed object, and its name and age are text and number values rather than references to nested mutable records. Later changes to a hypothetical original object's fields would not update those copied primitive values. That is narrower than saying copying always removes sharing. A shallow copy, one that copies only the outer fields, can retain aliases to nested objects. Such nested data is outside this schema, so the lab does not demonstrate general isolation of arbitrary input graphs.
The previous variance counterexample explains why a broad writable view can break a narrow promise. If a Cell<Cat> were improperly exposed as Cell<Animal>, the broader alias could write a Dog. The original Cat reader would then observe a value that violates its promise. The forbidden step is the writable alias conversion, not reading a Cat as an Animal. This is a hypothetical failure that the stipulated invariant cell rule rejects. The JSON analogy concerns preserving a field guarantee across writes, not adding Cat, Dog, or subtyping operations to the boundary validator.
Integer writes alone do not preserve the age policy
Later update to checked age 20
Still integer?
Still accepted age?
Replace with 21
Yes
Yes
Replace with 200
Yes
No, above 130
Replace with "unknown"
No
No, wrong representation
Prevent all later writes
Original integer retained
Original range retained
All updates are hypothetical. A design must preserve the actual range rule, not merely the broader representation category.
Separate a one-time check from an enduring invariant. An invariant is a property that every permitted state change preserves. To claim that age always remains in range, identify all ways to construct and update the stored value, then show how each preserves the range. If an external library can bypass those paths, that library belongs in the assumptions of the claim. Revalidating immediately before use may help for some designs, but it does not automatically solve concurrent changes or unchecked later uses. Those mechanisms are outside this local synchronous demonstration and require their own model.
Inspect the rules and their result
Compare a claimed type with an actual validation result
Unchecked assertion
Claim: User
A type assertion alone does not inspect these fields.
Validated result
No validated User result.
Rejected: age must be an integer from 0 through 130.
Presets replace the entire local JSON text; manual edits retain no previous success. Parsing accepts JSON syntax; validation checks only name and age. Extra fields are discarded from the returned object, not approved for use elsewhere. No payload is sent or stored. Maximum input length is 200 characters.
Claim
Needed evidence
JSON has required fields
Runtime schema check
Customer may act
Authorization decision
Value stays valid
Mutation/ownership policy
Program meets its purpose
Specification and corresponding verification
One type annotation cannot discharge every boundary obligation.
Read acceptance as a narrow result rather than an account decision
Use the String age preset in the boundary lab and compare its two panels. The unchecked assertion panel continues to say Claim: User, while the validated-result panel reports no validated result. The assertion label does not change with the payload because it represents a claim rather than an inspection. Choose Valid fields next. The result panel now contains only name and age. This difference isolates what runtime validation adds. It does not show a more powerful type assertion, and it does not establish that the named person exists or sent this payload.
Choose Extra role field and compare the accepted result with the textbox. The name and age remain, but role is absent from the returned object. Acceptance therefore applies to the selected projection, not a User object with administrator privileges. This distinction matters even when the extra field looks harmless. A future consumer might interpret it differently. By copying only the documented fields, this validator limits what it promises and returns. It neither rejects every unknown field nor certifies unknown fields for later use. The appropriate policy depends on the receiving application's requirements.
The same assertion label accompanies different validation results
Preset
Unchecked panel
Validation result
String age
Claim: User
Reject, age is text
Valid fields
Claim: User
Accept name and age
Extra role field
Claim: User
Accept name and age; discard role
These are existing presets. The assertion panel states a claim; only validation inspects whether name and age satisfy the schema.
For a manual contrast, edit the valid payload's age from 20 to 20.5, then to 130, then to 131. The first fails the integer rule, the second passes, and the third fails the range rule. Edits immediately recompute validation, so a previous successful result must not remain as if it described the changed text. There is no submit step or server response in this lab. The local input allows at most 200 UTF-16 code units, and the validator also rejects longer input. That length bound is an implementation boundary, separate from the age policy.
Name has its own useful contrast. A paper payload with name " " fails because removing surrounding whitespace leaves nothing. A payload with name " Mina " passes the nonblank test, but the returned name retains those spaces. The validator uses trimming to test blankness; it does not replace the returned string with a trimmed version. Thus acceptance does not imply normalized spelling. Similarly, a nonblank name of 31 ordinary letters exceeds the length policy even though it is text. These distinctions prevent a consumer from assuming transformations that the validation rule never performed.
Use Missing age and Out-of-range age to compare a missing fact with a false checked condition. Both reject, but the original payloads fail different obligations. Malformed JSON would fail earlier still, before any field inspection. The displayed error is evidence about the first reached failure, not a complete list of every possible defect. If name and age both violate the schema, fixing name may reveal an age error next. This does not mean the rule changed between edits. It reflects the validator's sequential inspection and early return on a failed condition.
Blankness testing does not normalize the returned name
Paper name field
Nonblank?
Within 30 code units?
Returned name
" "
No
Yes
No accepted result
" Mina "
Yes
Yes, six code units
" Mina "
31 ordinary letters
Yes
No
No accepted result
Quoted spaces are significant data here. Trimming tests whether text is blank; accepted text is copied without that transformation.
Finally, consider a fully accepted payload whose age is deliberately false and whose sender has no account permissions. Nothing in the displayed acceptance changes, because the validator has no evidence channel for either fact. Truthful age would require a trusted source or verification process, while an account update requires an authorization decision tied to an authenticated sender and target account. These are paper service obligations, not missing buttons to discover in the lab. The valid conclusion is about the returned data's checked representation and range, with no implication about identity or entitlement.
Make a precise conclusion
A useful conclusion names the language rules, inputs checked, and properties established. For example: under these finite core typing rules, the example has type Pair<Int, Bool>; under this JSON validator, the accepted result has a nonblank name and an integer age in the stated range.
Neither conclusion supplies authorization, a complete program specification, or universal safety. Use types to make obligations explicit and composition easier. Then test and validate the obligations that the chosen type system does not express, rather than replacing them with a broad “type-safe” label.
Match implementation evidence to the scope of the claim
A formal soundness theorem relates a language's typing rules to its evaluation rules. Earlier lessons introduced progress, the claim that a closed well-typed term is a value or can step, and preservation, the claim that a permitted step retains typing. Closed means that the term has no unresolved free names. Together, under the specified rules, these properties exclude defined stuck states. A stuck state is a nonvalue with no permitted next step. This theorem concerns the defined language, not every desirable property of every program described using the word typed.
The lesson engine has authored expression trees, an equality solver, type inference, and a separate bounded interpreter. It has no free-text parser, host evaluation, or generated machine code to audit. To examine its agreement, one can compare an inferred pair type with the interpreter's pair components on accepted examples. For the existing let-bound identity used on 3 and true, the inferred type is Pair<Int, Bool> and evaluation returns the corresponding pair. That is direct implementation evidence for one example. It does not quantify over every possible expression or establish a theorem about production compilers.
The existing let identity example supplies two different observations
Stage for the existing tree
Relationship or result
Generalize let-bound identity
forall a. (a → a)
Instantiate at first call
Fresh input/output variable becomes Int
Instantiate at second call
Different fresh variable becomes Bool
Final inferred result
Pair<Int, Bool>
Separate interpreted result
(3, true)
The type is inferred without using runtime values. Separate evaluation agrees on this accepted example, not on all possible programs.
Finite tests can target mechanisms rather than merely collect successful outputs. For unification, substitute a proposed solution back into every original equation and compare both sides. A failed conflicting pair may have a partial binding for a before discovering Int versus Bool. That partial binding must not count as a solution. For generalization, a captured outer variable must remain shared across uses, while independently quantified variables receive fresh instances. Each check probes a distinct obligation. The number of tests alone says less than which obligations they inspect and whether the expected answers were derived independently.
Resource failures require a different conclusion. This core bounds authored terms to 60 nodes and depth 12, integer literals to minus 100 through 100, and interpreter evaluation to 512 visits. A term that exceeds an input bound has not thereby been shown to contain incompatible types. An accepted term that reaches an evaluation limit has not thereby refuted preservation. The implementation stopped under its resource policy. A test report should separate rejected type relationships, unbound names, and limits, rather than combine them into a single category of unsafe programs or successful proofs.
An implementation audit also follows trusted assumptions outside the core rules. A validator may rely on JSON parsing; application code may rely on a library's declared interface; a compiler may allow documented compatibility trade-offs. The TypeScript compatibility reference explicitly discusses operations it accepts without a general soundness guarantee. That does not make its checks useless, but it prevents treating every accepted program as an instance of the earlier calculus's theorem. Ask which language, configuration, boundary operations, and mutation rules support the precise property. Evidence about one component cannot silently certify the whole chain.
Accepted Mina data leaves account claims undecided
Claim after accepting Mina, age 20
Evidence or missing obligation
Returned age is an integer in range
Established by field checks
Mina really is 20
Requires external factual evidence
Sender controls an account
Requires authentication evidence
Sender may update that account
Requires authorization policy and decision
Stored age stays valid later
Requires construction and update rules; no storage here
Each row concerns the same accepted payload. A schema conclusion cannot replace missing evidence about identity, permission, or later changes.
A defensible conclusion separates several claims that the fictional service merged. The local validator checks stated name and age rules and returns their projection. The finite inference examples receive types under the core rules, with evaluation performed separately on accepted cases. Neither mechanism authenticates a sender, authorizes an update, proves stored data remains unchanged, or establishes the intended business outcome. Those obligations need their own specifications and evidence. This separation makes the audit actionable. A failed claim identifies a missing check or assumption instead of dismissing all typing or granting a blanket guarantee that no implemented component actually supplies.
Exercises
Find the missing checks
A payload is syntactically valid JSON and passes the displayed schema. Which remain unproved: age is an integer, the age is truthful, and the sender may update an account?
Hint
Distinguish checked representation from external facts and permissions.
Worked answer
Claim
Status after this validator
Returned age is an integer in range
Established
Age describes the real person
Unproved
Sender is authorized
Unproved
The accepted object is deliberately narrower than the entire payload.
The validator establishes the integer/range property for the returned value. It does not establish truthful age or authorization. Those require separate evidence and policies. Ignoring extra fields also does not certify the original object as safe for every later use.
Write a bounded implementation claim
The inference engine passes thousands of tests. Can its documentation claim a formal proof of type soundness?
Hint
Tests inspect executions; a theorem quantifies over a defined language and semantics.
Worked answer
Evidence
What it supports
Example and property tests
Behavior on tested cases
Progress/preservation proof
A theorem for the specified calculus
Compiler integration audit
Agreement between implementation and assumptions
Different evidence supports different claims.
No. The tests support implementation behavior on the tested cases and invariants. A formal proof needs precise syntax, typing and evaluation rules, and an argument covering all relevant terms. The documentation should report the tests, their bounds, and the absence of a machine-checked proof.
Sources and further reading
Selected reference passages support the definitions and algorithms below. The examples, explanations, and implementations are original. Terminology and assumptions are stated within each lesson; source review is not an independent audit of this course. Optional links are not runtime dependencies.
Selected progress, preservation, and substitution statements. We do not claim to have independently checked the entire proof development or proved our implementation sound.
Selected structural compatibility and documented soundness trade-offs. Exact compiler behavior depends on flags and language version; our idealized variance lab is not a conformance test.