A Formalization of Core Why3 in Coq

Explore a groundbreaking conference talk from POPL 2024 that delves into formalizing the core of Why3 in Coq. Discover how researchers Joshua M. Cohen and Philip Johnson-Freyd tackle the challenge of providing strong guarantees for intermediate verification languages. Learn about their approach to creating a formal semantics in Coq for Why3's logic fragment, and understand its implications for program verification tools. Gain insights into the development of a correct-by-construction natural deduction proof system, its application in verifying parts of Why3's standard library, and the soundness proofs for two of Why3's transformations. Examine the potential of this work in bridging the gap between automated tools and foundational guarantees in program verification.