Wiki Health Audit and Gap Report

Problem/Feature Description

A developer named Marcus maintains a personal knowledge base wiki on programming language theory. The wiki has been growing organically for several months, and he suspects it's starting to drift—some pages may be out of date, important terms might be unlinked, and there could be gaps where the wiki references concepts without adequate sourcing.

Marcus wants a thorough health audit of the wiki. He prefers not to have the agent search the internet during the audit—he would rather know honestly which areas of the wiki lack coverage so he can decide what to read next. He wants a written report and the audit logged so he has a history of when health checks were performed.

Output Specification

Produce a lint audit of the wiki. The expected outputs are:

• A lint report saved as wiki/reports/health-audit-2026-04-06.md summarizing findings (orphan pages, stale claims, missing cross-references, important terms lacking pages, interesting connections)
• An updated wiki/log.md with a new log entry appended for this lint operation—the existing entries must remain exactly as they were
• Any gaps in sourcing should be honestly flagged in the report rather than filled with invented citations

Input Files

The following files are provided as inputs. Extract them before beginning.

=============== FILE: wiki/index.md ===============

Wiki Index

Topics

• Lambda Calculus — Formal system for computation using function abstraction and application
• Type Theory — Mathematical study of type systems in programming languages
• Curry-Howard Correspondence — Isomorphism between proofs and programs

People

• Alonzo Church — Mathematician who invented lambda calculus

=============== FILE: wiki/topics/lambda-calculus.md ===============

Lambda Calculus

Lambda calculus is a formal system developed by Alonzo Church in the 1930s to investigate computable functions.

Beta reduction

Beta reduction is the core evaluation rule: applying a function to an argument substitutes the argument for the parameter.

Church numerals

Numbers can be encoded in pure lambda calculus using Church numerals, where the number n is represented as a function applied n times.

See also

• Type Theory

=============== FILE: wiki/topics/type-theory.md ===============

Type Theory

Type theory provides a formal language for describing the types of values in programming languages. Martin-Löf type theory is a constructive foundation for mathematics.

The Curry-Howard correspondence connects type theory with formal logic.

Dependent types

Dependent types allow types to depend on values, enabling very precise specifications.

See also

• Curry-Howard Correspondence

=============== FILE: wiki/topics/curry-howard.md ===============

Curry-Howard Correspondence

The Curry-Howard correspondence establishes an isomorphism between:

• Types and propositions
• Programs and proofs
• Function application and modus ponens

This means that a type-correct program is equivalent to a proof of its type.

Historical note

This connection was independently discovered by Haskell Curry and William Howard.

=============== FILE: wiki/topics/linear-types.md ===============

Linear Types

Linear type systems enforce that each value is used exactly once, preventing aliasing and enabling safe memory management without garbage collection.

Rust's ownership system is inspired by linear type theory.

=============== FILE: wiki/people/alonzo-church.md ===============

Alonzo Church

Alonzo Church (1903–1995) was an American mathematician. He invented lambda calculus and proved the undecidability of the Entscheidungsproblem in 1936.

Church was the doctoral advisor of Alan Turing.

=============== FILE: wiki/log.md ===============

[2026-02-01] ingest | lambda-calculus-foundations

• Created: wiki/topics/lambda-calculus.md
• Created: wiki/people/alonzo-church.md
• Updated: wiki/index.md

[2026-02-14] ingest | type-theory-intro

• Created: wiki/topics/type-theory.md
• Created: wiki/topics/curry-howard.md
• Updated: wiki/index.md

[2026-03-20] ingest | linear-types

• Created: wiki/topics/linear-types.md