Quinn (Oct 19 2021 at 03:26): Quinn (Oct 19 2021 at 03:26):What's the latest on working with atotal codebases, besides "refactor the source into total haskell" which isn't in the economics this goaround and besides we have critical libraries that are turing complete? I'm thinking I can develop some workflow where I iteratively codegen with the cli and append things to edits file (or the paper refers to a preamble, but from tutorial usage I'm inferring that preamble got moved to edits file) when I don't like or don't think I can use the output. We think we're going to target a select few predicates about the code, so it only has to work for a subset. Am I just gonna have to get lucky that the engineers happened to write those subsets in total haskell?
Quinn (Oct 19 2021 at 03:37):I just did a test with
zip' :: [a] -> [b] -> [(a, b)]
zip' [] [] = []
zip' (x:xs) (y:ys) = [(x,y)] ++ zip' xs ys
and proved a conditional property (after codegenning) that length xs = length ys -> models2 Coq.List.zip zip' xs ys. It would be a workflow sort of like quickcheck, identifying preconditions and so on.
Stephanie Weirich (Oct 19 2021 at 12:53):There are several options for reasoning about partial functions with hs-to-coq. Identifying a precondition under which the function is total is a good approach. However, there are others as described in this paper (https://www.cis.upenn.edu/~sweirich/papers/containers-jfp.pdf) about our verification of the containers library and this paper (https://arxiv.org/abs/1910.11724) about our work with GHC.
Quinn (Oct 19 2021 at 16:24):excellent. Wasn't aware of the subsequent papers, was just going off of the first one. thanks!
Last updated: Feb 06 2023 at 05:03 UTC