How paranoid should I be that
hs-to-coq itself isn't correct? Should we run
hs-to-coq on the
hs-to-coq source to validate properties of it?
This paper: https://www.seas.upenn.edu/~sweirich/papers/containers-jfp.pdf describes some of the testing that we have done with hs-to-coq to gain confidence in its correctness. Proving the system correct would be a significant undertaking.
I see! the round trip testing suite correctness is exciting!
Last updated: Feb 06 2023 at 06:29 UTC