Well-Formedness Linter¶
Automated checker — instantiates Formal Derivation System Design
Mechanically scans candidate expressions and flags every one that violates the declared grammar, before it can enter derivation.
A Well-Formedness Linter is the runtime enforcer of legality. Where a grammar specification declares what a legal expression looks like, the linter is the automated tool that takes actual candidate expressions — one at a time or by the millions — and reports precisely which ones break the rules, and where. Its defining commitment is that it is a decidable gatekeeper, not an author: it never decides what should be legal, only whether a given string is legal under the grammar it is handed. By rejecting malformed input at the door, it acts as the front-line structural guardrail of the whole system, so that nothing downstream — no axiom application, no inference step — ever has to cope with syntactic garbage.
Example¶
A cheminformatics pipeline ingests millions of molecular structures encoded as SMILES strings (a real line notation for chemical graphs) before a property-prediction model runs on them. A malformed SMILES silently corrupts everything downstream, so a linter sits at the intake. For each string it checks the grammar: are ring-closure digits balanced, are bracketed atoms like [NH4+] well-formed, are bond symbols in legal positions? Handed C1CCCCC, it flags an unclosed ring bond at the opening 1 and rejects the record with a pointed message; handed c1ccccc1 (benzene) it passes it through. Run in the batch's continuous-integration step, the linter turns "some fraction of our structures are quietly broken" into a concrete, positioned list of rejects that a curator can fix — long before the model ever sees a garbage graph.
How it works¶
- Consume the grammar, don't author it. The linter is parameterized by the formation rules from the Formal Grammar Specification; it holds no opinion of its own about legality.
- Scan and locate. Each candidate expression is parsed against the grammar; on failure the linter reports the position and the rule violated, not merely a yes/no.
- Grade severity. Hard grammar violations are errors; softer convention breaches (naming, deprecated forms) may be warnings, so the gate can be strict on legality and advisory on style.
- Run at scale, side-effect-free. Because well-formedness is a decidable, terminating check, the linter can run in bulk, in CI, or as a pre-commit gate without altering the expressions it inspects.
Tuning parameters¶
- Strictness — which findings are blocking errors vs. non-blocking warnings. Stricter gates catch more but reject borderline-legal input; looser gates let more through for later stages to handle.
- Rule coverage — pure grammar conformance only, or additional house conventions layered on top. Broader coverage enforces more but risks false positives that annoy authors.
- Autofix vs. report-only — whether the linter proposes corrections or merely flags. Autofix speeds authors but can mask real intent errors.
- Incrementality — re-checking only changed expressions vs. the whole corpus. Incremental checking is fast but can miss violations introduced by context.
When it helps, and when it misleads¶
Its strength is failing fast and cheap: it catches the most basic class of error — illegal syntax — at the earliest, least costly moment, and it does so mechanically and uniformly across a corpus no human could review by hand.
Its failure mode is the seductive green checkmark. A lint-clean expression is legal, not correct: a perfectly well-formed SMILES can encode a chemically nonsensical molecule, just as a lint-clean program can be dead wrong. The linter is also only ever as good as the grammar it enforces — errors of legality baked into the grammar are invisible to it. The classic misuse is treating "passes the linter" as "is right," letting a syntactic gate stand in for validation it was never designed to do.[n1] The guarding discipline is to keep the linter's promise narrow and explicit: it is a necessary filter, never a sufficient one, and the real checks — validity, consistency, meaning — live in other mechanisms downstream.
How it implements the components¶
well_formed_expression_grammar— it operationalizes the grammar as an executable checker, turning the declarative formation rules into an automated accept/reject decision over real expressions.consistency_guardrail— it is the structural guardrail at the system boundary: a terminating, decidable gate that keeps malformed input out of the derivation kernel entirely.
It enforces the grammar but authors none of it: it does not declare the alphabet (symbol_vocabulary — that is its nearest twin, the Formal Grammar Specification, which defines the rules this linter merely applies) and it never licenses a derivation step (inference_rule_set — the Inference Rule Calculus).
Related¶
- Instantiates: Formal Derivation System Design — provides the mechanical gate that keeps only legal expressions in the system.
- Consumes: Formal Grammar Specification supplies the grammar the linter checks against.
- Sibling mechanisms: Formal Grammar Specification · Axiom Schema Catalog · Inference Rule Calculus · Rewrite or Transition Rule Engine · Proof Tree or Derivation Log · Mechanical Proof Checker · Metatheory Review Checklist · Consistency and Contradiction Test · Formal-System Change-Control Workflow
Editorial Notes¶
Form Classification¶
Form family: Assessment, Review & Assurance
Rationale: Well Formedness Linter is defined in the frozen evidence as: Mechanically scans candidate expressions and flags every one that violates the declared grammar, before it can enter derivation. Its operative deployed or enacted form is therefore Assessment, Review & Assurance.
Nearest alternative: Control, Automation & Runtime — Control, Automation & Runtime can support this mechanism, but the evidence centers the concrete operation described above rather than the alternative family's defining operation.
Review outcome: Adjudicated after independent review; medium confidence.
Origin Attribution¶
Primary origin: Computer Science & Software Engineering
Origin pattern: Cross-disciplinary synthesis
Present-day reach: Multi-domain
Rationale: Well formedness linter is rooted in computer science's formal languages, software, data structures, and automation tradition; historically that field developed the defining operation described here: mechanically scans candidate expressions and flags every one that violates the declared grammar, before it can enter derivation.
Related originating lineages:
- Engineering & Design — Engineering's quality, reliability, interface, and lifecycle tradition supplies an independent formative lineage for the mechanism's well formedness linter logic.
- Linguistics & Semiotics — Linguistics, pragmatics, and semiotic analysis has a distinct contributing or parallel lineage for the mechanism's defining operation: mechanically scans candidate expressions and flags every one that violates the declared grammar, before it can enter derivation.
- Mathematics — Mathematical modeling, proof, and abstract-structure practice has a distinct contributing or parallel lineage for the mechanism's defining operation: mechanically scans candidate expressions and flags every one that violates the declared grammar, before it can enter derivation.
Review resolution: The blind reviewers agree that computer_science is the primary origin and differ only on alternate origin disagreement, origin mode disagreement, domain reach disagreement, encyclopedia synthesis disagreement. I preserve every independently explained alternate from both records rather than imposing a numeric cap. I retain cross_disciplinary_synthesis because the combined evidence shows material contributions from several lineages. The broader reach of multi_domain records portability separately from historical provenance; encyclopedia_synthesis=true preserves the affirmative synthesis judgment where either reviewer identified one.
Encyclopedia synthesis: The exact catalogued form synthesizes established practice rather than reproducing a single standard historical label.
Review outcome: Reconciled after independent review; high confidence.
Notes¶
[n1] Lint — originally a Bell Labs tool by Stephen Johnson that flagged suspicious constructs in C source. The enduring lesson carried by its name: a linter reports forms that look wrong, which is a filter on legality and convention, never a proof of correctness. ↩