pith. sign in

arxiv: 2606.00220 · v1 · pith:CRMH7XZBnew · submitted 2026-05-29 · 💻 cs.PL · cs.AI

SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations

Eric Liang This is my paper

Pith reviewed 2026-06-28 19:25 UTC · model grok-4.3

classification 💻 cs.PL cs.AI
keywords tagless-finalweakest preconditionprogram semanticsbounded checkingexecutable semanticspredicate transformersimperative programs
0
0 comments X

The pith

A single tagless-final semantic interface generates both executable state transformers and weakest-precondition verification conditions from identical program definitions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Programs are written once against a semantic interface instead of an abstract syntax tree. That interface is interpreted in multiple ways to produce readable code, concrete execution, predicate transformers, and bounded counterexample search. The same definitions for five loop-free imperative programs generated executable transformers and verification conditions that passed bounded checking over domains up to 729 states. This keeps executable semantics, weakest-precondition artifacts, and bounded validation synchronized by construction. A reader would care because it reduces the duplication that normally arises when maintaining separate code for testing and formal verification.

Core claim

SEMBridge shows that object programs written against one tagless-final semantic interface for a loop-free imperative core with assignments, conditionals, assumptions, and assertions can be interpreted to yield both concrete executable state transformers and abstract weakest-precondition verification conditions, with the generated artifacts remaining synchronized and passing bounded checks over finite domains up to 729 states.

What carries the argument

The tagless-final semantic interface, which programs are written against once and then interpreted into executable, weakest-precondition, and bounded-checking meanings.

If this is right

  • The same program definitions produce both runnable state transformers and verification conditions.
  • Bounded checking validates the weakest-precondition artifacts over finite domains without separate code.
  • Executable semantics and predicate-transformer interpretations remain consistent by construction.
  • The architecture supports future addition of proof-assistant or SMT interpretations using the same interface.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach could extend to languages with loops if fixpoint or invariant interpretations are added to the interface.
  • Maintaining one source of truth might lower the cost of keeping tests and formal checks aligned during incremental changes.
  • Similar interfaces might apply to other domains where executable and analytic views of the same objects are needed.

Load-bearing premise

A single tagless-final semantic interface can be interpreted into both concrete executable semantics and abstract ones without loss of fidelity for the loop-free imperative core.

What would settle it

A loop-free program from the five examples, or a similar one, where the bounded checker over 729 states reports a counterexample that contradicts the weakest-precondition condition derived from the same definitions.

Figures

Figures reproduced from arXiv: 2606.00220 by Eric Liang.

Figure 1
Figure 1. Figure 1: SEMBridge architecture: one tagless-final object program is interpreted by multiple semantic back ends. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Verification-condition size and bounded checking cost for the SEMBridge prototype. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
read the original abstract

Formal methods provide rigorous accounts of program behavior, but practical software engineering often works through executable libraries, tests, and incremental design. This paper presents SEMBridge, a small tagless-final framework for generating weakest-precondition and bounded-checking interpretations from the same executable object programs. Instead of committing a program semantics to one abstract syntax tree and then writing separate traversals, object programs are written once against a semantic interface and interpreted into multiple meanings: readable code, concrete execution, predicate transformers, bounded counterexample search, and future proof-assistant or SMT back ends. The Python prototype implements a loop-free imperative core with assignments, conditionals, assumptions, and assertions. Across five example programs, the same tagless-final definitions generated executable state transformers and verification conditions that passed bounded checking over domains up to 729 states. The contribution is not a Scala code-generation system or a new verifier, but a compact architecture for keeping executable semantics, weakest-precondition artifacts, and bounded validation synchronized.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper presents SEMBridge, a tagless-final framework for a loop-free imperative core (assignments, conditionals, assume/assert) in which object programs are written once against a semantic interface and interpreted into executable state transformers, weakest-precondition predicates, and bounded model-checking artifacts. The central empirical claim is that the same definitions, when interpreted, produced verification conditions that passed bounded checking on five example programs over state spaces up to 729 states, thereby keeping executable semantics and verification artifacts synchronized by construction.

Significance. If the result holds, the work shows a compact, reusable architecture for maintaining consistency between executable semantics and formal artifacts via tagless-final style, which is a practical strength for incremental development. The Python prototype for the core language is explicitly credited as providing an accessible, reproducible implementation. The contribution is architectural rather than a new soundness theorem or scalable verifier, and its scope is deliberately limited to loop-free programs.

major comments (1)
  1. [Abstract] Abstract: the claim that the five examples 'passed bounded checking over domains up to 729 states' is load-bearing for the central empirical result, yet the manuscript supplies no implementation details, derivation steps for the interpretations, or error analysis that would allow assessment of whether the tagless-final interface preserved fidelity between the executable and abstract interpretations.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and constructive feedback. We address the single major comment below and will revise the manuscript accordingly to strengthen the presentation of the empirical results.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that the five examples 'passed bounded checking over domains up to 729 states' is load-bearing for the central empirical result, yet the manuscript supplies no implementation details, derivation steps for the interpretations, or error analysis that would allow assessment of whether the tagless-final interface preserved fidelity between the executable and abstract interpretations.

    Authors: We agree that the manuscript would benefit from expanded implementation details to support the central claim. In the revised version we will extend the Implementation section with explicit derivation steps showing how the tagless-final interface is instantiated for the weakest-precondition and bounded-checking interpreters. We will also add an appendix containing the Python source for all five examples together with a short error-analysis subsection that discusses how fidelity between the executable state-transformer and predicate interpretations was checked (via direct comparison on the small state spaces). These additions will allow readers to reproduce and assess the synchronization property. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper describes a tagless-final architecture for a loop-free imperative core, where object programs written against a single semantic interface are interpreted into executable state transformers, weakest-precondition predicates, and bounded-checking artifacts. The five examples are reported to pass checks up to 729 states. This outcome follows directly from the tagless-final encoding itself (multiple interpreters over the same definitions) rather than any derivation, fitted parameter, or self-citation chain. No equations, uniqueness theorems, ansatzes, or renamings of known results appear. The central claim is an empirical demonstration of synchronization by construction of the style, with no load-bearing step that reduces to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract provides no information on free parameters, axioms, or invented entities.

pith-pipeline@v0.9.1-grok · 5696 in / 1168 out tokens · 54758 ms · 2026-06-28T19:25:41.009393+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

22 extracted references · 14 canonical work pages

  1. [1]

    An axiomatic basis for computer programming

    C. A. R. Hoare, "An axiomatic basis for computer programming," Communications of the ACM, vol. 12, no. 10, pp. 576-580, 583, 1969. doi:10.1145/363235.363259

    work page doi:10.1145/363235.363259 1969

  2. [2]

    Guarded commands, nondeterminacy and formal derivation of programs,

    E. W. Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs," Communications of the ACM, vol. 18, no. 8, pp. 453-457, 1975. doi:10.1145/360933.360975

    work page doi:10.1145/360933.360975 1975

  3. [3]

    G. D. Plotkin, A Structural Approach to Operational Semantics, DAIMI FN-19, Aarhus University, 1981

    1981

  4. [4]

    Definitional interpreters for higher-order programming languages,

    J. C. Reynolds, "Definitional interpreters for higher-order programming languages," in Proceedings of the ACM Annual Conference, vol. 2, pp. 717-740, 1972

    1972

  5. [5]

    Building domain-specific embedded languages,

    P. Hudak, "Building domain-specific embedded languages," ACM Computing Surveys, vol. 28, no. 4es, 1996. doi:10.1145/242224.242477

    work page doi:10.1145/242224.242477 1996

  6. [6]

    When and how to develop domain-specific languages,

    M. Mernik, J. Heering, and A. M. Sloane, "When and how to develop domain-specific languages," ACM Computing Surveys, vol. 37, no. 4, pp. 316-344, 2005. doi:10.1145/1118890.1118892

    work page doi:10.1145/1118890.1118892 2005

  7. [7]

    Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages,

    J. Carette, O. Kiselyov, and C.-C. Shan, "Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages," Journal of Functional Programming, vol. 19, no. 5, pp. 509-543, 2009. doi:10.1017/S0956796809007205

    work page doi:10.1017/s0956796809007205 2009

  8. [8]

    Folding domain-specific languages: Deep and shallow embeddings,

    J. Gibbons and N. Wu, "Folding domain-specific languages: Deep and shallow embeddings," in Proceedings of ICFP 2014, pp. 339-347. doi:10.1145/2628136.2628138

    work page doi:10.1145/2628136.2628138 2014

  9. [9]

    Efficient generation and simulation of synthetic text corpora for scalable information retrieval testing,

    R. S. Puranik, "Bridging formal methods and software engineering through a tagless-final embedded DSL for program semantics," in 2025 IEEE 2nd International Conference on Information Technology, Electronics and Intelligent Communication Systems (ICITEICS), Bengaluru, India, 2025. doi:10.1109/ICITEICS64870.2025.11341094

    work page doi:10.1109/iciteics64870.2025.11341094 2025

  10. [10]

    Felleisen, R

    M. Felleisen, R. B. Findler, and M. Flatt, Semantics Engineering with PLT Redex. Cambridge, MA: MIT Press, 2009

    2009

  11. [11]

    Ott: Effective tool support for the working semanticist,

    P. Sewell, F. Zappa Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. Strnisa, "Ott: Effective tool support for the working semanticist," Journal of Functional Programming, vol. 20, no. 1, pp. 71-122, 2010. 7 doi:10.1017/S0956796809990293

    work page doi:10.1017/s0956796809990293 2010

  12. [12]

    An overview of the K semantic framework,

    G. Rosu and T. F. Serbanuta, "An overview of the K semantic framework," Journal of Logic and Algebraic Programming, vol. 79, no. 6, pp. 397-434, 2010. doi:10.1016/j.jlap.2010.03.012

    work page doi:10.1016/j.jlap.2010.03.012 2010

  13. [13]

    Boogie: A modular reusable verifier for object-oriented programs,

    M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino, "Boogie: A modular reusable verifier for object-oriented programs," in FMCO 2005, LNCS 4111, pp. 364-387, 2006. doi:10.1007/11804192_17

    work page doi:10.1007/11804192_17 2005

  14. [14]

    Dafny: An automatic program verifier for functional correctness,

    K. R. M. Leino, "Dafny: An automatic program verifier for functional correctness," in LPAR-16, LNCS 6355, pp. 348-370,

  15. [15]

    doi:10.1007/978-3-642-17511-4_20

    work page doi:10.1007/978-3-642-17511-4_20

  16. [16]

    Why3: Where programs meet provers,

    J.-C. Filliatre and A. Paskevich, "Why3: Where programs meet provers," in ESOP 2013, LNCS 7792, pp. 125-128, 2013. doi:10.1007/978-3-642-37036-6_8

    work page doi:10.1007/978-3-642-37036-6_8 2013

  17. [17]

    Formal verification of a realistic compiler,

    X. Leroy, "Formal verification of a realistic compiler," Communications of the ACM, vol. 52, no. 7, pp. 107-115, 2009. doi:10.1145/1538788.1538814

    work page doi:10.1145/1538788.1538814 2009

  18. [18]

    Symbolic execution for software testing: Three decades later,

    C. Cadar and K. Sen, "Symbolic execution for software testing: Three decades later," Communications of the ACM, vol. 56, no. 2, pp. 82-90, 2013. doi:10.1145/2408776.2408795

    work page doi:10.1145/2408776.2408795 2013

  19. [19]

    Harmonizing metadata of language resources for enhanced querying and accessibility,

    Z. Liang, "Harmonizing metadata of language resources for enhanced querying and accessibility," in 2024 5th International Conference on Computers and Artificial Intelligence Technology (CAIT), pp. 642-650. IEEE, 2024

    2024

  20. [20]

    Efficient representations for high-cardinality categorical variables in machine learning,

    Z. Liang, "Efficient representations for high-cardinality categorical variables in machine learning," in 2025 International Conference on Advanced Machine Learning and Data Science (AMLDS), pp. 1-11. IEEE, 2025

    2025

  21. [21]

    Enhanced estimation techniques for certified radii in randomized smoothing,

    Z. Liang, "Enhanced estimation techniques for certified radii in randomized smoothing," in 2025 8th International Conference on Artificial Intelligence and Big Data (ICAIBD), pp. 375-384. IEEE, 2025

    2025

  22. [22]

    Automating date format detection for data visualization,

    Z. Liang, "Automating date format detection for data visualization," in 2025 International Conference on Advanced Machine Learning and Data Science (AMLDS), pp. 756-764. IEEE, 2025

    2025