2 subscribers • 1 video on Hallway
Advanced. Deep dive for people who know the field.
206 views6 years ago1 recommendation
Programming languagesComputer scienceHaskellCompilers and interpretersFormal methods and verification
Yao Li discusses translating core parts of the GHC compiler into Coq using hs-to-coq to verify invariants despite a formalization gap.
If a codebase is so big and complicated that complete mechanical verification is intractable, can we still benefit from verification methods? We show that by constructing 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.What people say. Recommended for its perspective on the formalization gap when verifying Haskell programs with hs-to-coq.
u/Syrakin r/haskell • Recommends
On “Tutorial: Verify Haskell Programs with hs-to-coq”