Quinn (Oct 22 2021 at 16:14): Quinn (Oct 22 2021 at 16:14):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?
Stephanie Weirich (Oct 22 2021 at 16:55):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.
Quinn (Oct 22 2021 at 17:47):I see! the round trip testing suite correctness is exciting!
Last updated: Feb 06 2023 at 06:29 UTC