I guess I’m a little unclear on what this post was supposed to have shown? The original premise seems to have been that “People claim FP is more intuitive/more natural/better than IP, which is equivalent to saying it’s easier to make formal proofs in FP over IP.” Whether or not FP is better or worse than IP, I have a hard time seeing these two claims as related? Something that’s easy or difficult to prove doesn’t make it easy or difficult to write simply, to the standard of a normal software engineer.
To me, this post provides pretty clear evidence that making a claim like: “Writing Haskell means that if it compiles, I know it’s correct,” is wrong. It’s shown that types alone aren’t enough to prove correctness and that proving correctness is laborious and hard, whether you have a heap to deal with, or not.
I agree that making the jump from “intuition” to “provably correct” is not obviously related. But, by comparing the implementation of a formally verified proof in a FP language, vs. a formally verified proof in an IP language, it becomes pretty clear that formal verification is hard no matter what. The FP folks had just as much trouble as the IP folks. The FP folks wrote just as many pages of code as the IP folks did, i.e. FP didn’t provide more intuition, and wasn’t obviously better.
One thing I completely forgot to say in the article was how hard it was for me to write these functions. The first two took about an hour each, the last one took about three. This was with no experience with writing code proofs, too.
In this case what we’re measuring is “difficulty in writing a proof for an imperative algorithm” with “difficulty in writing a proof for a purely functional algorithm.”
Congratulations on not only doing your first proven programs but making waves as you did do. Im curious, though, what you read or watched to learn how to do the formal specs. Esp if you think other beginners would find it helpful.
The FP folks had just as much trouble as the IP folks.
I agree, I think that’s the part that violates a widely held belief: many people believe intuitively that FP code should be easier to formally verify than imperative code, because of referential transparency etc. I’m not sure this is a widespread view among people who do verification, but it’s fairly common view among regular FP programmers.
I guess I’m a little unclear on what this post was supposed to have shown? The original premise seems to have been that “People claim FP is more intuitive/more natural/better than IP, which is equivalent to saying it’s easier to make formal proofs in FP over IP.” Whether or not FP is better or worse than IP, I have a hard time seeing these two claims as related? Something that’s easy or difficult to prove doesn’t make it easy or difficult to write simply, to the standard of a normal software engineer.
To me, this post provides pretty clear evidence that making a claim like: “Writing Haskell means that if it compiles, I know it’s correct,” is wrong. It’s shown that types alone aren’t enough to prove correctness and that proving correctness is laborious and hard, whether you have a heap to deal with, or not.
I agree that making the jump from “intuition” to “provably correct” is not obviously related. But, by comparing the implementation of a formally verified proof in a FP language, vs. a formally verified proof in an IP language, it becomes pretty clear that formal verification is hard no matter what. The FP folks had just as much trouble as the IP folks. The FP folks wrote just as many pages of code as the IP folks did, i.e. FP didn’t provide more intuition, and wasn’t obviously better.
One thing I completely forgot to say in the article was how hard it was for me to write these functions. The first two took about an hour each, the last one took about three. This was with no experience with writing code proofs, too.
In this case what we’re measuring is “difficulty in writing a proof for an imperative algorithm” with “difficulty in writing a proof for a purely functional algorithm.”
Congratulations on not only doing your first proven programs but making waves as you did do. Im curious, though, what you read or watched to learn how to do the formal specs. Esp if you think other beginners would find it helpful.
I agree, I think that’s the part that violates a widely held belief: many people believe intuitively that FP code should be easier to formally verify than imperative code, because of referential transparency etc. I’m not sure this is a widespread view among people who do verification, but it’s fairly common view among regular FP programmers.