docs: what a deliberately awkward page taught us - #365
Merged
Conversation
A public obstacle web page — 40 pages built to be hard to automate — was used as a corpus to find gaps in the grammar. 28 are solved; this records the other 12 with reasons, because "hard" is not a reason and a gap nobody has named gets rediscovered. The score is not the point. Four separate defects it surfaced share one shape: an operation answered a narrower question than the one asked, and the narrower answer was always yes. The fifth is systemic — every shape the grammar had declined was being improvised into a recording by the model fallback, because a decline that exists only in prose is a decline the engine does not implement. Also records what the corpus was worth mechanically: three obstacles that looked like they needed control flow did not, two that looked like they needed pointer precision did not, and one feature made 16 of 22 then-open obstacles expressible. Plus the rule that cost two wrong predictions — read the value off the page, do not predict it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
Adds a single consolidated documentation artifact (docs/obstacle-course.md) capturing what the “deliberately awkward” obstacle-course corpus revealed about flowproof’s grammar/recording gaps, with grouped reasons for the remaining unsolved cases to prevent repeated rediscovery.
Changes:
- Introduces a new obstacle-course writeup describing the solved/unsolved split and the underlying failure-patterns the corpus surfaced.
- Documents the 12 unsolved obstacles grouped by root cause (no completion path, step latency, drag mechanism, vacuous pass, product decision).
- Records practical lessons about randomness vs. branching and “read from the page, don’t predict” for seeded PRNG cases.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+3
to
+5
| A public obstacle web page — 40 pages, each built to be hard to automate, | ||
| each scoring itself by calling its own `obstacleCompleted()` — was used as a | ||
| corpus to find gaps in flowproof's grammar. This is what it found, so the |
Comment on lines
+63
to
+64
| 23292. The mouse dispatch landed 4 drops in 8 against a real jQuery UI | ||
| sortable, and `headless_chrome` 1.0.22 exposes no `Input.dispatchDragEvent`. |
Comment on lines
+51
to
+52
| 87912 accepts a generated value for 2 seconds. 16384 deletes its record | ||
| after 5. A step costs ~3.2s (measured; see `docs/authoring.md`), so both |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Docs only. One artifact replacing findings currently scattered across a dozen PR bodies.
What it is
A public obstacle web page — 40 pages built to be hard to automate — was used as a corpus to find gaps in the grammar. 28 are solved. This records the other 12 with reasons, because "hard" is not a reason and a gap nobody has named gets rediscovered.
Why it is worth a file
The score is the least interesting output. Four separate defects the corpus surfaced share one shape:
is visiblechecked that a selector resolved — and adisplay:noneelement resolves. A cell was addressed by countingths againsttds — and returned a real cell with real text from the neighbouring column.Selectfell through to typing — and typing into a<select>is itself a prefix search, so it selected some other option. The published schema omitted two shipped action types — and the conformance fixture exercised neither.The fifth is systemic:
recordfalls back to the LLM author for anything the rules cannot parse, so every shape the grammar had declined was being improvised into a recording. A decline that exists only in prose is a decline the engine does not implement.The unsolved 12, grouped by cause
Input.dispatchDragEvent.The part I would most want kept
Three obstacles that looked like they needed control flow did not — pinned, each is a straight line. Two that looked like they needed pointer precision did not — the targets are ordinary DOM elements. Much of what looks like branching is randomness in disguise, and one feature (
browser.random) made 16 of the 22 then-open obstacles expressible.And the rule that cost two wrong predictions before it was learned: read the value off the page, do not predict it. Simulating the seeded PRNG to precompute values failed twice, because other page scripts consume draws first — the seed pins the sequence, not the position.
Notes
🤖 Generated with Claude Code