On Tue, Feb 12, 2013 at 4:47 PM, Nehal Patel <nehal.a...@gmail.com> wrote: > > A few months ago I took the Haskell plunge, and all goes well... > ... snip ... > And so my question is, that in 2013, why isn't this process a full fledged > part of the language? I imagine I just don't know what I'm talking about, so > correct me if I'm wrong, but this is how I understand the workflow used in > practice with program derivation: 1) state the problem pedantically in code, > 2) work out a bunch of proofs with pen and paper, 3) and then translate that > back into code, perhaps leaving you with function_v1, function_v2, > function_v3, etc -- that seems fine for 1998, but why is it still being > done this way?
There is no one-stop shop for this sort of stuff. There are plenty of ways to show equivalence properties for certain classes of programs. I am unsure why you believe people tend to use pen and paper - machines are actually pretty good at this stuff! For example, I have been using Cryptol lately, which is a functional language from Galois for cryptography. One feature it has is equivalence checking: you can ask if two functions are provably equivalent. This is used in the examples to prove that a naive Rijndael implementation is equivalent to an optimized AES implementation. You might be asking why you can't do this for Haskell. Well, you can - kind of. There is a library called SBV which is very similar in spirit to Cryptol but expressed as a Haskell DSL (and not really for Crypto specifically.) All SBV programs are executable as Haskell programs - but we can also compile them to C, and prove properties about them by using an SMT solver. This is 'free' and requires no programmer intervention beyond stating the property. So we can specify faster implementations, and properties that show they're equivalent. SMT solvers have a very low cost and are potentially very useful for certain problems. So there's a lot of good approaches to tackling these problems in certain domains, some of them more automated than others. You can't really provide constructive 'proofs' like you do in Agda. The language just isn't meant for it, and isn't really expressive enough for it, even when GHC features are heavily abused. > What I'm asking about might sound related to theorem provers, -- but if so ,I > feel like what I'm thinking about is not so much the very difficult problem > of automated proofs or even proof assistants, but the somewhat simpler task > of proof verification. Concretely, here's a possibility of how I imagine > the workflow could be: I believe you are actually precisely talking about theorem provers, or at least this is the impression I get. The reason for that is the next part: > ++ in code, pedantically setup the problem. > ++ in code, state a theorem, and prove it -- this would require a revision to > the language (Haskell 201x) and perhaps look like Isabella's ISAR -- a > -structured- proof syntax that is easy for humans to construct and understand > -- in particular it would possible to easily reuse previous theorems and > leave out various steps. At compile time, the compiler would check that the > proof was correct, or perhaps complain that it can't see how I went from step > 3 to step 4, in which case I might have to add in another step (3b) to help > the compiler verify the proof. > ++ afterwards, I would use my new theorems to create semantically identical > variants of my original functions (again this process would be integrated > into the language) Because people who write things in theorem provers reuse things! Yes, many large programs in Agda and Coq for example use external libraries of reusable proofs. An example of this is Agda's standard library for a small case, or CoRN for Coq in the large. And the part about 'leaving things out' and filling them in if needed - well, both of these provers have had implicit arguments for quite a while. But you can't really make a proof out of axioms and letting the compiler figure out everything. It's just not how those tools in particular work. I find it very difficult to see the difference between what you are proposing and what people are doing now - it's often possible to give proof of something regardless of the underlying object. You may prove some law holds over a given structure for example, and then show some other definitive 'thing' is classifed by that structure. An example is a monoid, which has an associative binary operation. The /fact/ that operation is associative is a law about a monoids' behavior. And if you think about it, we have monoids in Haskell. And we expect that to hold. And then actually, if you think about it, that's pretty much the purpose of a type class in Haskell: to say some type abides by a set of laws and properties regardless of its definitive structure. And it's also like an interface in Java, sort of: things which implement that basic interface must abide by *some* rules of nature that make it so. My point is, the intuition we have about what it means for programs to be 'equivalent' or have 'structure' is very deep mathematically and computationally. We use these properties to reason about our programs, and their behavior and relation to other programs, and perhaps for the sake of efficiency (but mostly, just for sanity.) So there's naturally a ridiculously huge amount of work into this field of program correctness and derivation! But Haskell isn't a language where you provide proofs, you can only provide evidence. And monoids aren't very interesting on their own anyway. So: how do we classify and codify program behavior in ways for 'equivalence'? Are there reasons for this beyond equivalence checking? I think at heart your question is asking: is there a rigorous notion in which we can describe properties of Haskell programs, prove them, and then prove other things for Haskell programs as we know them today? I think the answer for right now is, it's limited. And probably not what you want. There are a lot of approaches. Isabelle can compile Haskell code into Isabelle for example, so you can prove stuff there. Zeno is an automated proof system for Haskell 98. There's been research into Haskell "contracts" for defining compile-time contract enforcement. You can use SBV to prove things about symbolic, bit-precise programs, etc. You can just ignore the fact that Haskell has `undefined' and `seq` and friends and reason/prove things in a 'Total Haskell' subset of the language[1]. You can also provide fairly rich types in Haskell to say things, but at a certain point it becomes a bit crazy (Cryptol does things Haskell/SBV can't really do easily or at all, for example.) In practice that means all these approaches are not meant for grand-scale stuff. They could certainly work in the short run, though. You may want to really give a theorem prover a run if you haven't already. Some of these include Agda, Coq, Isabelle and more recently Idris. Finally, I think Jan Stolarek offers a very interesting perspective: some compilers and libraries *already* make your programs faster through proofs! Typical list deforestation through the 'foldr/build' rule is a more general result about the behavior of catamorphisms. I wrote about this myself a while ago[2]. So, GHC can use that to eliminate intermediate data structures - so maybe your slow reference isn't that slow! [1] http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html [2] http://neocontra.blogspot.com/2013/02/controlling-inlining-phases-in-ghc.html -- Regards, Austin _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe