Whitefoot is a programming language designed as a harness for AI agents. It serves human-directed systems development with implementation delegated to agents, using constraints, explicit interfaces, and machine-checked proofs to guide authors toward safe, efficient programs. The compiler checks required source evidence and erases it before execution; writers have no unchecked escape hatch. The specification defines the exact guarantees and trusted boundary.
The target is a serious research compiler that compiles real programs and lets us test language and performance ideas. Whitefoot uses restrictions, interfaces, and writer guidance to make ordinary implementations fall into efficient, verifiable classes and to expose architectural mistakes early. The goal is useful default performance, not a guarantee that every accepted program is globally optimal.
Ease of manual source authorship is not an independent goal. Additional source and proof effort can be worthwhile when they improve performance or correctness, while usable feedback and enough information to complete the task still matter. Changing the intended author opens alternatives; experiments must establish which mechanisms work under their stated conditions.
The constitution owns the objectives and tradeoffs; Agent instructions own project priorities and workflow.
Read the material that owns the question you are working on:
| Question | Source |
|---|---|
| What does the language admit? | Active kernel specification |
| What does this compiler implement, and how do I run it? | Running the compiler below; the conformance report states the implemented surface |
| What are the project goals and design principles? | Constitution |
| How do I work on a branch and prepare a merge? | AGENTS.md; CLAUDE.md is the identical alternate entry |
| Which writer forms should I try? | Patterns |
| How should I investigate, verify, and maintain documentation? | Engineering practice |
| Why was a design chosen? | Design trees, with reasons and refused alternatives |
| Which research questions and experiments could be useful? | Ideas |
| What defects and implementation costs are known? | Todo |
Research and dated essays provide evidence and ideas; they do not add approval requirements. The reading and authority rules are in AGENTS.md.
- compiler/: the Rust compiler, LLVM emission, and native runtime support.
- spec/: the active language and its immutable version archives.
- tests/: normative conformance evidence, recorded-verdict snapshots, executable programs, and code-generation evidence.
- docs/: principles, writer guidance, engineering practice, and reference material.
- research/: investigations and experiments with their designs, measurements, and rejected alternatives.
- mcts_mem/: frozen historical decision record, being moved into
design/and deleted when that is complete. - design/: live design decisions with their reasons, and the procedure that maintains them.
- governance/: archive-protection hooks and specification-change design evidence. The old approval ledger is retired.
- .github/: CI and the pull-request template.
- archive/: frozen historical material. Active source, builds, tests, and tools do not depend on it.
From compiler/:
cargo run --bin whitefootc -- source.wf -o program
cargo run --bin whitefootc -- --emit-llvm source.wf
cargo run --bin whitefootc -- --par source.wf -o programwhitefootc accepts an ordered bundle of source files. --no-overlap selects
the exact sequential reference lowering and cannot be combined with --par.
--par-ledger and --stack-ledger print their reports; name the LLVM output
with -o when a report and emitted LLVM would otherwise share stdout.
--par takes three grain controls. --par-scalar-leaf-limit N|off moves or
removes the default threshold that keeps scalar leaves of at most 16
nonconstant operations out of compute offers; --par-sequential-refusal runs
a refused offer's callee in its sequential clone; --par-recursive-frontier auto|N|off sets the starting budget of a recursive component's clone family,
where auto, the default, asks the runtime, N from 1 to 32 pins it at
compile time, and off emits no family so every node offers. whitefootc --help prints the full usage. At run time WF_WORKERS selects compute
participation; WF_STACKS is inert.
From the repository root:
make check
make install-hooks # optional: catch immutable-spec edits earliermake check is the canonical complete gate and prints stage timings. Its
stage inventory is defined in the root Makefile and
compiler Makefile. For a shorter development feedback
loop:
make static
make -C compiler format lint
make -C compiler test-unit
cargo test --manifest-path compiler/Cargo.toml --profile gate --locked --offline --lib semantic::tests::source_proofsUse a test filter matching the responsibility changed; source_proofs above
is one example. The gate profile keeps debug assertions and overflow checks
while optimizing the compiler's analysis work. The complete gate is still
required on the exact revision merged into main.
The gate workflow runs those stages on Linux and macOS. Additional I/O host checks and benchmarks own their platform-specific evidence. A green run describes its tested revision and coverage; it is not a proof of completeness or the absence of known defects. Conformance reports distinguish passing cases, expected compiler failures, and pending support.
Specification identity is derived from the active file's bytes by compiler/build.rs. The work-branch and specification amendment rules are stated once in AGENTS.md.
Whitefoot is available under the MIT License.