RFD-0015 — Surface naming prefers PL idiom over proof-assistant idiom

Question

Argon’s expressivity ceiling is Lean-class (tier:fol, tier:modal, tier:mlt admit propositions-as-types-equivalent reasoning). Should the surface vocabulary borrow from proof-assistant traditions (Lean / Coq / Agda) or from programming-language traditions (Rust / TypeScript / Haskell)?

Decision

When a construct, attribute, or keyword in Argon has both a programming-language analogue and a proof-assistant analogue, the surface uses the PL term. Target mental model is Rust / TypeScript / Haskell / Scala — not Lean / Coq / Agda — even when the underlying semantics derive from proof-assistant foundations.

Examples:

• derive (PL: data-flow / Datalog) over lemma or theorem (proof-assistant).
• query and mutation (PL: GraphQL / database) over goal and tactic.
• pub and module-internal visibility (PL: Rust) over private / protected (Java) or Local / Global (Coq).
• unsafe { … } for the FOL escape (PL: Rust) over Sorry or Admitted (proof-assistant; though #[unproven] and #[assumed] capture related but distinct concepts).
• Singular keywords (input, not inputs; require, not requires).

Rationale

Daily-driving feel matters more than expressivity ceiling. Most Argon code is structural / closure / recursive tier — the ergonomic ground floor. Authors at that tier are working on tax law, lease accrual, GAAP recognition. Naming the language for proof-assistant audiences would have made the daily 90% feel foreign.

Lean expressivity, Rust feel. The expressivity ceiling is Lean-class because the semantic substrate supports it, not because we want every modeler to think in proof-theoretic terms. The surface should fade into the background for the structural tier and only surface its expressiveness when an author deliberately reaches for it.

Singular keywords scan as English. “require this, do that, retract those, return result” reads like instructions. “requires X, does Y” forces the reader to mentally drop the s to parse the structure.

No Lean references in examples. Even when an example draws inspiration from a Lean mechanization, the example doesn’t reference Lean by name in tracked artifacts. The reader’s mental model stays in PL territory.

Consequences

• New language surface (keywords, attributes, decorator names) goes through this filter. PL term wins ties.
• Existing surface that drifted toward proof-assistant idiom (some early decorator names) gets renamed when noticed.
• Documentation and the book describe constructs in PL terms, even when they have proof-theoretic interpretations.
• Reasoner output describes derivations in PL-friendly language (“derived”, “applied”), not proof-theoretic language (“inferred”, “concluded”).