This is my nod to the excellent technical work being done at TC39 (link). I am not aware of anything else like this being done stateside, so if you would like to set this repo up as a community hub, please reach out.

ScriptCert Pearl

ScriptCert is a small, readable "pearl" that demonstrates the core idea behind a formally verified compiler for a JavaScript fragment.

It borrows its engineering shape from CompCert:

• define source and target semantics explicitly,
• implement a simple compiler pass,
• prove semantic preservation for that pass,
• keep the trusted base small and obvious.

It also mirrors the spirit of TC39 proposals:

• language behavior should be specified clearly,
• changes should be staged and reviewable,
• implementation artifacts should stay aligned with the specification.

What this prototype verifies

The current pearl models a tiny JavaScript-like expression language:

• numbers (42)
• addition (a + b)
• subtraction (a - b)
• multiplication (a * b)
• unary negation (-a)
• optional chaining on some(...) wrappers (receiver?.value as opt_chain)
• pattern matching with constant branch results (match)

The compiler translates expressions into a stack-machine program.

In coq/JsPearl.v, we prove that running compiled code yields the same value as directly evaluating the source expression:

run (compile e) [] = Some [eval e]

This is the central semantic-preservation theorem for this miniature compiler.

A local audit of the TC39-linked surface in this repository found no semantic drift that requires changing compile_correct; the current proof still matches the implemented optional-chaining and constant-result pattern-matching subsets.

Repository layout

• coq/JsPearl.v: AST, source semantics, target machine, compiler, and correctness proof.
• src/scriptcert.py: executable mirror of the same definitions.
• src/main.py: small CLI for compiling and running sample expressions.
• tests/test_scriptcert.py: regression and property-style checks over sample trees.
• docs/COMPCERT_NOTES.md: CompCert best-practice notes used in this pearl.
• docs/TC39_NOTES.md: TC39 process notes plus the feature-trace matrix.
• THIRD_PARTY_NOTICES.md: third-party standards/process attributions.
• LICENSE: canonical BSD 2-Clause licensing for this repository.

TC39 feature-trace matrix

Canonical matrix: docs/TC39_NOTES.md

Feature	ScriptCert status	Proof status
Arithmetic expressions (Number, +, -, *, unary -)	Implemented	compile_correct proved
Optional chaining (?.)	Implemented (pearl subset)	compile_correct proved
Pattern matching	Implemented (constant-result pearl subset)	compile_correct proved

Quick start

Run the executable tests:

python3 -m unittest discover -s tests -v

Try the CLI:

python3 src/main.py --expr '["match", ["opt_chain", ["some", ["add", 3, 4]]], [[["num", 7], 10], ["undef", 20], ["_", -1]], 0]'

Expression forms currently supported:

• arithmetic: add, sub, mul, neg
• optional chaining subset: some, opt_chain
• pattern matching subset: match with arms [[pattern, constantValue], ...]

Expected output includes:

• source evaluation result,
• emitted stack instructions,
• target execution result,
• a semantic-preservation check.

Coq proof check (optional)

If Coq is installed:

coqc coq/JsPearl.v

Verify against TC39 directly

This repo now includes a machine-readable TC39 manifest in docs/tc39_manifest.json and a verifier in src/tc39_audit.py.

Run a direct check against the live tc39/proposals repository:

python3 -m src.tc39_audit

Or use the Makefile target:

make tc39-check

Optional local checkout or submodule

You can use a git submodule for reproducible, pinned snapshots of tc39/proposals, but note the trade-off: a submodule is not automatically "live" tracking. You must periodically update it.

Add the submodule:

git submodule add https://github.com/tc39/proposals.git vendor/tc39-proposals

Verify against that local snapshot:

python3 -m src.tc39_audit --proposals-dir vendor/tc39-proposals

Refresh the snapshot later:

git submodule update --remote --merge vendor/tc39-proposals
python3 -m src.tc39_audit --proposals-dir vendor/tc39-proposals

Recommended workflow:

• use the live check when you want the freshest TC39 status,
• use a submodule when you want reviewable, reproducible upstream snapshots in this repo.

Approach in plain language

This project starts from the behavior we want to preserve, not from optimization tricks.

1. We define exactly what source programs mean.
2. We define exactly what target code means.
3. We write a compiler that is simple enough to reason about structurally.
4. We prove, by induction on syntax, that the meanings agree.

That is the same high-level discipline used by CompCert, scaled down to a JavaScript-focused pearl that can evolve with TC39-driven language design.

License

This project is licensed under the BSD 2-Clause License. See LICENSE.