REVIEW 1 cited by
Embracing a mechanized formalization gap
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a deliberate mechanized formalization gap we can shrink and simplify the model until it is manageable, while still retaining a meaningful, declaratively documented connection to the original, unmodified source code. Concretely, we translate core parts of the Haskell compiler GHC into Coq, using hs-to-coq, and verify invariants related to the use of term variables.
Forward citations
Cited by 1 Pith paper
-
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
In an ablation across five LLMs and two Rocq projects, informed prompts with dependencies and in-file context produced the highest proof success (up to 52% of hs-to-coq theorems), and success fell sharply without context.
Discussion (0). Continue with ORCID to comment.