Type theory gives precise rules for classifying expressions, constructing mathematical objects and, in richer systems, representing propositions with proofs. It supports programming-language safety and machine-checked mathematics, but every guarantee depends on a clearly stated type system, context and trusted assumptions.
This guide begins with typed functions and structured data, develops induction and the propositions-as-types correspondence, then explains dependent vectors, equality, constructive logic, proof assistants and their limitations. Original worked cases expose the difference between proving a formal property and validating real-world data.
Choose a type-theory learning route
Typing judgments and simple constructors · Chapters 1–8 · Start here
Induction, logic and evidence · Chapters 9–17 · Start here
Dependent types, equality and proof · Chapters 18–25 · Start here
Foundations, scope and study · Chapters 26–30 · Start here
Chapter index · Original examples · Proof and runtime checks · Connected subject roots
Complete chapter index
Typing judgments and simple constructors
- 1. Type theory connects objects, evidence and rules
- 2. Type theory and programming language theory differ in scope
- 3. Judgements tell us what a statement claims
- 4. Contexts make assumptions visible
- 5. Base types and constructors build larger types
- 6. Function types describe input and output expectations
- 7. Application is checked against the argument type
- 8. Products, records and projections
Induction, logic and evidence
- 9. Sum types and exhaustive case analysis
- 10. Inductive types express finite constructed data
- 11. Proof by induction follows the constructor structure
- 12. Identity and equality require a chosen formal meaning
- 13. The Curry–Howard correspondence
- 14. Implication becomes a function construction
- 15. Conjunction and disjunction have different evidence
- 16. Universal quantification and dependent functions
- 17. Existential claims as dependent pairs
Dependent types, equality and proof
- 18. Dependent types can index values by other values
- 19. Length-indexed vectors clarify the contract
- 20. Type equality and transport
- 21. Universes organise types of types
- 22. Constructive and classical logic differ in principles
- 23. Decidable propositions and Boolean computations
- 24. Termination, normalisation and their boundaries
- 25. Proof assistants have a trusted kernel
Foundations, scope and study
- 26. Refinement types capture selected predicates
- 27. Proof irrelevance is not universal across all calculi
- 28. Homotopy type theory broadens the view of identity
- 29. Proof obligations should be chosen for real value
- 30. A practical learning path and common questions
A type-level claim is not every kind of correctness
| Statement | What it can establish | What remains |
|---|---|---|
| f : A → B | Input-output typing under rules | Correct domain outcome and permitted effects |
| Vector A 3 | Length-indexed structure | Truth, completeness and provenance of contents |
| Proof of P | P under accepted logic and axioms | Whether premises represent the world |
| Value is range-checked | Defined numeric bound | Correct authority, unit and interpretation |
| Machine-checked theorem | Derivation accepted by checker | Specification and implementation correspondence |
1. Type theory connects objects, evidence and rules
Type theory studies formal systems in which expressions have types and well-formed operations follow specified rules. Types may describe numbers, functions, structured data and, in richer systems, propositions and proofs. The field underpins programming languages, formal verification and alternative mathematical foundations.
The central discipline is to ask which judgement is being established, under which assumptions and by which inference rule. Writing that an expression has a type does not prove every claim a real application might make about the expression. A correct formal result is valuable because its scope is precise rather than because its notation looks authoritative.
2. Type theory and programming language theory differ in scope
Programming language theory investigates syntax, semantics, evaluation, binding, types and the behaviour of whole languages. Type theory focuses more deeply on types as formal objects, judgements, constructions, logical relationships and proof principles. The subjects overlap, and many tools developed in one are used in the other.
The Programming Language Theory root covers evaluation and compiler semantics. This guide builds a conceptual route from simple typed expressions to the propositions-as-types correspondence, dependent types and proof assistants. Distinguish an implementation language’s features from the formal calculus used to justify a theorem.
3. Judgements tell us what a statement claims
A common typing judgement Γ ⊢ e : T means that under context Γ, the expression e has type T according to the rules of a particular system. Γ lists relevant assumptions such as variable declarations. Other judgements can express that a type is well formed or that two expressions are equal under a specified equality notion.
The notation does not stand alone: the grammar and typing rules decide what is derivable. A proof checker must know which context, universe, effects and computational rules apply. Do not infer that a variable typed as LearnerId necessarily names the correct real learner. The judgement is formal evidence within its declared model.
4. Contexts make assumptions visible
A typing context records available variables and their types. If Γ contains x:Nat and y:Nat, a rule for natural-number addition may derive Γ ⊢ x+y : Nat. If y is instead a string and the language supplies no relevant conversion, that derivation is not justified.
Context assumptions are part of the claim. A theorem about well-typed closed terms may not apply unchanged to a term containing untyped external inputs. When teaching, write the context before tracing an expression; hidden assumptions cause many apparent contradictions in type reasoning.
5. Base types and constructors build larger types
Simple systems may include Boolean, natural-number and unit types. Type constructors build new types: products combine components, sums represent alternatives and function types represent transformations. A pair (3,true) can have type Nat×Bool under an appropriate calculus.
The structure describes permitted values and operations rather than guaranteeing the values are scientifically meaningful. A temperature represented as a floating-point number may still have the wrong unit. Richer domain types can prevent some confusions when the representation and operations are designed correctly.
6. Function types describe input and output expectations
A function type A→B represents a transformation accepting an argument of type A and producing a result of type B in the relevant model. A typed lambda expression λx:A.e has such a type if the body e has type B when x:A is assumed.
The arrow by itself does not assert that a programme terminates, is side-effect-free or meets a separate business requirement in every programming-language setting. Some formal calculi enforce stronger properties than ordinary executable languages. State which system supplies each guarantee instead of assuming all function arrows mean exactly the same thing.
7. Application is checked against the argument type
If Γ ⊢ f:A→B and Γ ⊢ a:A, then a function-application typing rule can conclude Γ ⊢ f a:B. The rule is about the compatibility of two derived judgements. Passing a value of an unrelated type cannot be justified by it without an additional conversion or subtyping rule.
A useful exercise is to derive the result type line by line. One type error can identify a precise mismatch, but a successful derivation need not prove that a function computes the correct answer for its intended domain. Type correctness and functional correctness are related but distinct jobs.
8. Products, records and projections
A product type A×B contains a pair whose first component has type A and second component type B. Projection rules retrieve each component with its corresponding type. Records generalise the idea with named fields, and structures can encode reusable invariants depending on the language.
A two-field record containing a pupil ID and assessment mark does not establish that the mark belongs to that pupil. Referential integrity, authorisation and assessment provenance are separate requirements. The type system can describe a record’s shape while other evidence protects the truth of its relationship.
9. Sum types and exhaustive case analysis
A sum type A+B represents one of two tagged alternatives, often described by constructors such as Left and Right. Elimination requires a rule for each branch to produce an appropriately typed result. An optional value can similarly represent None or Some(value), discouraging accidental treatment of absence as a numerical zero.
Exhaustive pattern checking can reveal unhandled alternatives after a model changes, but a catch-all case may still conceal a mistaken real-world decision. Define the meaning of each constructor. A test result marked NotAttempted, for example, should not quietly enter the same branch as Failed.
10. Inductive types express finite constructed data
Inductive definitions specify values through constructors, such as zero and successor for natural numbers or nil and cons for lists. Their elimination principles permit case analysis and induction. The type’s definition supplies a structural foundation for recursive functions and proofs.
An inductive list is a formal structure, not automatically an efficient storage layout. A proof by list induction can be valid for all finite lists in the chosen calculus, while a deployed parser can still fail because it supplies malformed or incorrectly decoded data. Keep mathematical structure and implementation boundaries distinct.
11. Proof by induction follows the constructor structure
To prove a property P(n) for every natural number under the standard inductive definition, prove P(0) and prove P(n)→P(n+1). Structural induction on lists similarly handles the empty list and the case of extending a shorter list.
The statement being proved must quantify over the relevant objects, and the induction hypothesis must match the recursive structure. Checking P(0), P(1) and P(2) is not an induction proof. A proof assistant can help enforce the logical steps, but only for the proposition it has been given.
12. Identity and equality require a chosen formal meaning
Type systems may distinguish definitional or judgemental equality—expressions recognised as equal through computation or permitted conversion—from propositional equality, which can have proof objects. The distinction varies by calculus and implementation. Similar-looking expressions need not be convertible under one system’s reduction rules.
For example, evaluating a simple addition of numerals may yield a definitionally equal normal form, while a general algebraic identity can require a separate proof. The fact that two values print identically does not establish equality in every dependent type. Say which equality judgement is intended.
13. The Curry–Howard correspondence
In propositions-as-types interpretations, propositions can be represented as types and proofs as inhabitants of those types. Implication corresponds to function construction; conjunction resembles products; and disjunction resembles tagged sums in suitable constructive settings. This connects programming and logic through formal rules.
The correspondence is not an assertion that ordinary type-checked business software proves all its promises. It depends on the calculus, accepted axioms and meaning assigned to a type. The Lean 4 theorem-proving text develops the relationship in a proof assistant.
14. Implication becomes a function construction
To prove A→B constructively, one may assume evidence of A and produce evidence of B. Under propositions-as-types, a function of type A→B does just that: it transforms an inhabitant of A into an inhabitant of B under the relevant rules.
An implication can be true in a formal logic without asserting that someone has run a physical experiment confirming B. The formal proof establishes a logical relationship given premises; whether a premise accurately describes the world remains an empirical or domain-governance question.
15. Conjunction and disjunction have different evidence
Evidence for A∧B requires evidence of both A and B under a constructive product-like interpretation. Evidence for A∨B identifies one branch and supplies evidence for it through a sum-like construction. A proof by cases must handle each possible constructor correctly.
The distinction is valuable in software workflows. A status field saying VerifiedOrApproved does not mean both conditions hold. To make a protected action require both, the representation and rules must reflect conjunction rather than a permissive alternative.
16. Universal quantification and dependent functions
A universally quantified proposition ∀x:A, P(x) can correspond in dependent type theory to a function that produces evidence of P(x) for each x:A. The output type depends on the input value. This is more expressive than an ordinary function returning one fixed result type.
A claim about every element of a mathematically defined domain differs from a claim about every physical case. If an input parser excludes invalid dates, the theorem may concern only accepted values. State the quantified domain and the boundary that checks whether real inputs belong to it.
17. Existential claims as dependent pairs
A proposition asserting that some x:A satisfies P(x) can be represented constructively by a dependent pair containing a witness x and evidence of P(x). Sigma types generalise ordinary product types because the second component’s type depends on the first.
For a simple educational example, the witness may be an integer n and a proof that n+n=6. A pair carrying n=3 and the appropriate equality proof supports the existential statement. It does not imply that every nearby numerical problem has such a witness.
18. Dependent types can index values by other values
In dependent type theory, types may mention values, such as Vector A n for a sequence of n elements of type A. A matrix operation can require compatible dimensions in its interface so mismatched sizes are excluded within the formal language’s rules.
This is useful when the dimensions are known or checked at the correct boundary. A vector indexed by length three does not prove the measurements inside it are calibrated or belong to the intended participant. Dependent types strengthen selected structural guarantees; they do not replace empirical evidence or access authority.
19. Length-indexed vectors clarify the contract
A function append on vectors may have a type stating that joining a vector of length m with one of length n produces a vector of length m+n. The output-length relationship becomes part of the type, not an informal comment. A proof can follow the recursive structure of the first vector.
An implementation must still correctly decode the external source into a verified vector of the claimed length. If an import silently drops a value, a theorem about the internal vector remains true while the data-processing job is wrong. The user-visible result needs both boundary validation and proof.
20. Type equality and transport
When a dependent type refers to a value, replacing that value with an equal one may require a formal transport or rewrite operation. A vector of length n+0 can be recognised as equivalent to one of length n only according to the calculus’s computation and equality rules.
Some identities reduce definitionally, while others need a lemma. The difference is a common source of proof-assistant friction, not evidence that mathematics is inconsistent. A learner should inspect whether the required equality is computationally immediate or a proposition requiring proof.
21. Universes organise types of types
Many dependent type theories use universe levels to organise the types in which other types live. This helps avoid unrestricted self-reference leading to logical inconsistencies in naive foundational systems. The details differ between proof assistants and formal calculi.
A universe level is not a classroom grade or a physical hierarchy of objects. It is part of a formal system’s consistency and typing discipline. When moving a proof between systems, universe polymorphism and cumulativity assumptions may change whether a particular construction is accepted.
22. Constructive and classical logic differ in principles
Constructive type theories typically interpret proofs as constructions and do not necessarily provide the law of excluded middle for every proposition as a computationally usable rule. Classical principles can often be added or used in dedicated logical contexts with consequences for computation and proof interpretation.
A constructive proof of A∨¬A generally requires information sufficient to choose a side in the relevant calculus. A classical proof may reason differently. It is misleading to claim that one style makes the other automatically erroneous; state the logic and what computational content is expected.
23. Decidable propositions and Boolean computations
A decidable proposition comes with a procedure or evidence that establishes it or its negation in an appropriate constructive system. A Boolean is a two-valued data object; relating a Boolean test to a proposition requires a correctness theorem.
A function returning true on examples is not proof that it decides every legal input. Distinguish a terminating decision procedure with a verified relation to the proposition from a heuristic classifier returning a binary guess. This matters when a programme’s answer is used as proof of eligibility or access.
24. Termination, normalisation and their boundaries
Some typed calculi enforce termination of all definable computations or enjoy strong normalisation under their formal rules. This can support proof checking and consistent constructive interpretation. Real programming languages may include general recursion, exceptions or external actions that do not terminate.
Do not infer that every programme written in a language featuring dependent types must terminate. Proof assistants may separate trusted logical fragments from effectful executable code. A totality or normalisation theorem needs the precise system and trusted assumptions stated.
25. Proof assistants have a trusted kernel
Tools such as Lean, Rocq and Agda implement ways to express formal statements and build checked derivations. Tactics can automate proof construction, while a smaller trusted checker verifies the resulting proof term or derivation under the tool’s design.
The trust boundary still includes the kernel, axioms, compiler or extraction path when executable guarantees are claimed. A checked theorem can be about an incorrect specification. Study the proof statement, accepted axioms and input assumptions rather than counting the number of green checkmarks.
26. Refinement types capture selected predicates
A refinement type can describe values satisfying a predicate, such as integers in a specified range. Depending on the language and checker, a developer may need to supply proof obligations or runtime validation to establish the refinement.
A score in 0 to 100 is structurally bounded, but its numeric validity does not establish assessment comparability, correct student identity or authorised processing. This is a clear example of how a strong type prevents one class of error while leaving other obligations to governance and measurement.
27. Proof irrelevance is not universal across all calculi
Some type systems distinguish propositions that are treated as proof-irrelevant in a particular universe from types whose different inhabitants carry computational information. Other systems use intensional equality or higher structures in which identification has richer meaning.
Before declaring two proofs interchangeable, identify whether the calculus supplies proof irrelevance, which universe and equality notion apply, and what operations can inspect proof terms. Assertions that seem obvious under a particular assistant may not transfer unchanged into a different foundational system.
28. Homotopy type theory broadens the view of identity
Homotopy type theory draws connections between type theory and homotopy-theoretic structures. Its development includes ideas such as univalence and higher inductive types under defined mathematical rules. It offers a rich alternative approach to reasoning about types and paths of identity.
A beginner need not master homotopy groups to learn ordinary dependent types. The Homotopy Type Theory book is a primary resource, but its specialised assumptions should not be mixed casually with a different proof assistant’s default theory. Learn the foundational system before transporting theorems.
29. Proof obligations should be chosen for real value
Formal types can protect array bounds, protocol states, dimensions and other precise constraints. Proving every conceivable property may be impractical, while choosing only trivial properties creates the appearance of rigour without preventing meaningful errors.
Start from a user requirement and a plausible defect. Encode the part that mathematics can check, document the environmental conditions and test the implementation boundary. A proof that a financial amount is nonnegative does not make an unauthorised charge acceptable; the contract must represent the right outcome.
30. A practical learning path and common questions
Does a type signature prove a function meets every specification? No. Is dependent type theory merely adding many generic types? No; types can depend on terms under its rules. Is every proposition decidable in constructive logic? No. Does a machine-checked proof guarantee the physical world behaves as modelled? No.
Begin with typing contexts, functions and pairs. Derive simple judgements, then prove a property by induction and explore propositions-as-types. Use small examples in Lean or Agda before moving to dependent vectors, equality transport and universes. The enduring standard is a precise theorem whose meaning readers can explain.
← Previous · Original examples
Twenty-six original type and proof cases
1. A function application has mismatched types
A context contains f:Nat→Bool and x:Nat. The application f x has type Bool under the function application rule. Supplying a string y instead does not justify the same derivation without another rule. The point is to show which premise is missing rather than merely report ‘type error’.
2. A pair carries two different kinds of values
The expression (3,true) can have type Nat×Bool in a simple calculus. Projecting the first component yields a natural number; projecting the second yields a Boolean. That does not imply any interpretation of 3 as a valid examination result.
3. A sum requires the correct branch
An operation has a result type Success+Error. Code handling only Success is incomplete unless another rule deals with Error. The tagged construction makes the alternative visible, but the user-facing error message still needs appropriate design.
4. A type derivation hides a false external premise
A parser claims that a supplied record has type ValidExamEntry, but it trusts a caller-provided flag without checking the record. A downstream proof about valid entries may be formally correct while the boundary violates its assumption. Establish the constructor’s actual validation rule.
5. A length-indexed append protects a structural result
Joining a vector of length two with one of length three should produce length five in an appropriate vector calculus. A dependent signature can express that relation. The proof does not establish that five elements are scientifically correct observations.
6. A proposition needs a witness
To prove that some natural n satisfies n+n=6 constructively, give n=3 and a derivation of the equation. Merely asserting that such a number probably exists does not inhabit the intended dependent pair.
7. The proof of implication uses an assumption
Given a construction that converts evidence of A into evidence of B, the corresponding function has type A→B. The statement does not by itself supply a value of A or assert that A is empirically true.
8. A conjunction is not disjunction
A protected action requires verified identity AND valid authorisation. A field representing either condition as sufficient encodes a different policy. Use product-like evidence for the intended conjunction and test the access boundary.
9. Induction is more than several observed cases
A student verifies a formula for n=0,1,2,3 and calls it proved. A formal induction requires the base case and a step showing the property for n+1 from the hypothesis for n. A proof assistant can check that general argument.
10. A propositional equality differs from conversion
Two expressions may compute to the same normal form under definitional reduction. A broader algebraic equality may need a lemma. Choose the appropriate equality notion when rewriting dependent types.
11. A type universe is not a value-level grade
A learner tries to store an ordinary school year number as if it were a universe level, confusing levels of formal syntax. Universes organise types, while a Year type can represent school years. The names do not imply the same mathematical role.
12. Proofs can have different computational status
A system may erase proof-irrelevant evidence during execution while retaining data whose constructors matter to computation. Whether that is sound depends on the formal calculus and language rules. Do not generalise across proof assistants without checking their designs.
13. An ordinary type does not prove an access right
A function receives a value of type UserId and retrieves a record belonging to another user. The ID is well typed but not authorised. Security and ownership require an additional validated relation.
14. A dependent vector relies on correct decoding
A file contains four measurements, but the importer drops one and constructs a length-three vector. A function proved correct for Vector Measurement 3 still uses an incomplete dataset. The external source-to-type boundary must be checked.
15. A Boolean classifier is not a proof
A model returns true when it predicts that a document is authentic. That result is an estimate, not a formal inhabitant of a proposition establishing authenticity. A proof would require valid evidence and rules connecting it to the claim.
16. A partial recursive function lacks totality
A function loops indefinitely on some legal inputs but its type looks like Nat→Nat in a general-purpose language. The type alone may not guarantee termination. State the calculus and proof obligations before claiming total correctness.
17. A tactic closes a goal under an unexpected axiom
A proof assistant accepts a theorem using a user-declared axiom that is not justified for the intended model. The proof term is checkable relative to that axiom, but the real-world or foundational conclusion may not follow without it. Inspect assumptions.
18. A refinement describes the wrong interval
An assessment value uses a refinement requiring 0≤score≤100. An exam actually permits bonus marks above 100 under an official rule. A formally enforced invariant can reject valid inputs if the domain specification is wrong. Review the real assessment rules.
19. Equality transport needs the right identity
A vector has length n+0 but a function expects length n. A suitable lemma can relate these indices, depending on reduction rules. Renaming the vector in source text without proving the equality does not change its dependent type.
20. An impossible type should not be fabricated
A proof goal requires an inhabitant of the empty type. In a consistent constructive calculus there is no closed inhabitant under ordinary rules. Inserting an unjustified axiom could make the proof pass while undermining soundness. Reject the step rather than invent evidence.
21. A nonempty list needs construction evidence
An operation requires a NonemptyList type. Passing a plain list without checking whether it contains an element is not enough. A smart constructor can return either proof of nonemptiness or an explicit error.
22. A proof of sorted output cannot repair wrong labels
A theorem shows an algorithm returns an ordered list. The source records contain two learners merged under the same identifier. Sorting correctness remains true for the input list while the real report is false. Provenance and identity need separate validation.
23. A classical proof may not produce an algorithm
An argument uses excluded middle to show some property holds in a classical setting. It may not provide the constructive witness or executable decision procedure a programme needs. Distinguish existence and computational extraction under the chosen logic.
24. Two assistant versions disagree on default axioms
A formal proof is moved between assistants with different foundational rules or universe conventions. The statement may not check unchanged. Document source tool version, axioms, imported libraries and exact theorem rather than claiming automatic portability.
25. A validated schema is not a verified institution
A record satisfies a dependent type enforcing three required fields, but the issuing school is fraudulent. Field presence and logical structure cannot certify external identity or factual reliability. Use authoritative source checks beyond the type.
26. A classroom proof becomes a software claim
Students prove that adding two natural numbers returns a natural in a simple calculus. A production system handles fixed-width integers, signed overflow and untrusted text input. The original theorem is a sound educational step, but deployment requires reasoning about the actual number representation and boundaries.
Sixteen further proof, evidence and changed-context cases
1. A list whose elements are all valid can still be the wrong list
A dependent type expresses that every item in a list satisfies a validation predicate. A library system accidentally supplies records from the wrong course, and all of them satisfy that predicate. The theorem does not establish course identity or selection correctness. Add a suitable index or source relationship to the specification if that is part of the requirement. This case shows why adding proof strength in one dimension cannot replace stating the right real-world question.
2. A proof of nonzero length is not a proof of completeness
An importer constructs a nonempty vector of laboratory readings. It proves at least one element exists but the intended experiment required twelve timed observations. A successful nonempty proof is too weak for the evidence job. Specify the expected sample structure, timestamps and reasons for missingness. A stronger type may help enforce count, but validity of instrument readings and representativeness still require other checks.
3. An equality proof depends on an unrecorded conversion
A numerical routine converts a measurement to another unit before comparing it with a threshold. Its theorem assumes both quantities use the same unit, but the input layer fails to convert one field. Formal arithmetic reasoning proceeds correctly on mismatched representations. Use types that retain units where feasible, test unit conversions and record source metadata. The lesson is to connect the theorem’s assumptions with verified measurements instead of trusting a numerical field’s bare type.
4. A custom axiom makes every goal look easy
A novice declares an axiom that gives evidence of any proposition and then observes every proof obligation closing. The proof assistant is doing exactly what the added premise permits; the resulting system no longer demonstrates meaningful consistency guarantees. Examine axioms and trusted foundations before celebrating proof automation. An explicit assumption is part of a formal theorem, and unsupported assumptions cannot turn a fictional claim into evidence.
5. A programme with general recursion breaks a normalisation expectation
A student learns strong normalisation for a restricted typed calculus, then writes a recursively defined service that keeps calling itself. The language permits general recursion, so the earlier theorem is not directly applicable. Distinguish proof-language terms from effectful or potentially divergent executable code. Where termination matters, use an appropriate decreasing measure, total fragment or verified protocol-level liveness argument. The mathematical fact remains useful within its stated calculus.
6. A dependent interface improves matrix safety but not numerical stability
A matrix multiplication function requires compatible dimensions using dependent types. It rules out some shape mismatches, yet multiplying poorly scaled values can still overflow or lose precision under fixed hardware arithmetic. Test conditioning, numerical bounds and actual representations separately. Type-level dimensions and numerical analysis protect different parts of the computation. A fully typed procedure can still produce an inaccurate scientific estimate if floating-point effects and input quality are ignored.
7. A proof term is correct but the exported source is stale
A theorem is checked against a particular source definition. Later, another team updates the executable implementation without rerunning the proof or establishing a refinement relation. The theorem remains valid about the old abstract function, not necessarily the new deployed code. Record code versions, proof dependencies and relevant build outputs. An assurance claim needs a maintained relationship between the verified specification and the actual service that users operate.
8. An existential witness is not the authorised witness
A type contains a pair representing an identifier and evidence that it satisfies a syntactic format. The application uses the pair to release a student’s record. Format validity does not prove that the requester is entitled to access that identifier. Introduce separately verified authorisation evidence tied to the requesting identity and purpose. A valid dependent pair answers only the proposition that its second component establishes.
9. An appeal process cannot be replaced by a proof checker
An automated examination system proves that every assigned grade is computed according to a published formula. A pupil appeals because the source marks were attributed to the wrong script. The arithmetic theorem does not investigate handwriting identity, marking fairness or procedural rights. Maintain the proof for calculation correctness while preserving independent review and correction processes for factual and institutional errors. Strong formal systems should make disputes easier to diagnose, not remove legitimate human recourse.
10. A classical existence theorem is mistaken for a terminating programme
An institution needs an algorithm that constructs a feasible timetable. A formal argument establishes that some timetable exists under classical reasoning, but supplies no effective procedure or acceptable runtime bound. Existence alone does not meet the operational requirement. Identify whether the proof is constructive, whether an extraction mechanism applies and whether the resulting algorithm fits resources and actual constraints. Mathematical truth and computational feasibility are related but not interchangeable.
11. A type abbreviation erases an important conceptual difference
A programme uses the same primitive string type for source DOI, local student number and cryptographic signature identifier. All satisfy the generic String type, making accidental mixing easy. Define separate nominal types or appropriate refinements where the application needs the distinction. Even after doing so, external authority and identifier validity require independent verification. The value of the type system lies in expressing meaningful differences at the places where mistakes would matter.
12. A closed proof is built from an inconsistent context
A theorem is derived using assumptions Γ that include contradictory statements about the same property. The proof may be accepted relative to those assumptions while conveying little legitimate information about the intended system. Check assumption consistency and provenance rather than merely the final goal. If a model declares that every participant both has and lacks authorisation, formal deduction cannot repair the defective specification. Review premises before using a proof to justify action.
13. An encrypted value passes a type check but cannot be decoded
A storage API returns a value labelled EncryptedRecord and the programme type-checks, but the necessary key or algorithm version has changed. The type alone does not guarantee recoverability or authenticity. Add appropriate runtime error handling, key governance and recovery checks. A type may identify what kind of object was expected while operational tests determine whether it can fulfil its legitimate purpose.
14. An identity proof is used across different formal systems
A result established in one type theory is copied into a system with different equality and universe assumptions. Symbols look similar, but inference rules may not match. Transporting the theorem requires a precise interpretation or translation and verification in the target theory. The task is not solved by reproducing the statement as text. Formal portability is an argument about meaning and rules, not a visual resemblance of notation.
15. A proof-relevant construction is treated as proof-irrelevant
A programme retains a pair of witnesses that encode distinct derivation paths, but a refactoring erases one under the assumption all proofs are interchangeable. The validity of erasure depends on the proof system, type and observational semantics. Inspect whether the evidence carries computational information or is confined to a proof-irrelevant universe. A property of one proposition sort should not be used as a universal rule for all typed values.
16. A proof checker becomes the final step rather than the first
A school software team formalises an important invariant about access to learner results. The proof passes, and the team then tests real authentication, importing, revocation and audit trails, discovering a gap between modelled identities and issued credentials. They revise the contract and rerun verification. This is a successful use of type theory: one precise guarantee becomes part of a larger, corrigible assurance process rather than a reason to stop checking reality.
Connected eduKate Gold Standard guides
Formal mathematics and languages
Implementation and evidence
Authoritative type-theory textbooks and proof references
- Software Foundations — Logical Foundations
- Programming Language Foundations in Agda
- Theorem Proving in Lean 4
- Homotopy Type Theory Book
- Software Foundations — Programming Language Foundations
The formal examples use simplified calculi and invented records. A statement about a real system requires appropriate validation of source data, authority, software implementation and the specific proof assistant’s assumptions.
Continue through The Gold Standard, Education and Learning Transfers into Life, and How X Works.