formal methods & functional programming
Hi, I have been searching papers about tha raltionship between formal methods in software engineering and functinal programmming, but i haven't found enough information. can u hel me?. Thanks Abigail. __________________________________________________ Correo Yahoo! Espacio para todos tus mensajes, antivirus y antispam ¡gratis! Regístrate ya - http://correo.espanol.yahoo.com/
I can't think of any Haskell papers about ``formal methods'' in
software engineering, but many papers and books talk about proving
program correctness, which is difficult in traditional, imperative
languages (which is why it is probably not stressed as much as
//testing// is in formal software methods). Paul Hudak, in the
textbook, The Haskell School of Expression
(http://www.amazon.com/gp/product/0521644089/104-7074974-5852762?v=glance&n=283155)
writes a lot about proving program correctness (especially induction
on recursive algorithms) for Haskell and purely functional programs,
reasoning mathematically.
If you want to do strenuous testing, you can use "QuickCheck:
Automatic Specification-Based Testing":
http://www.cs.chalmers.se/~rjmh/QuickCheck/
A professor I had at Caltech researches formal methods in constructing
reliable software systems, specifically using robust programming
language and compiler technology (in this case OCaml).
http://mojave.caltech.edu/
Jared.
On 1/14/06, Abigail
Hi, I have been searching papers about tha raltionship between formal methods in software engineering and functinal programmming, but i haven't found enough information. can u hel me?. Thanks Abigail.
__________________________________________________ Correo Yahoo! Espacio para todos tus mensajes, antivirus y antispam ¡gratis! Regístrate ya - http://correo.espanol.yahoo.com/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- jupdike@gmail.com http://www.updike.org/~jared/ reverse ")-:"
Abigail
Hi, I have been searching papers about tha raltionship between formal methods in software engineering and functinal programmming, but i haven't found enough information.
I don't think there are any papers, but Galois Connections employs Haskell and formal methods such as proof checkers in our work. You might email for more information: http://www.galois.com/ peace, isaac
Abigail wrote:
Hi, I have been searching papers about tha raltionship between formal methods in software engineering and functinal programmming, but i haven't found enough information.
Functional programming in pure functional languages like Haskell can help to make programs easier to reason about - but it doesn't _remove_ the need for formal methods. For example, there are laws about certain classes such as Monad and Monoid which all instances of those classes must follow in order to be considered "proper" Monads or Monoids. However, in order to reason about functions defined over all Monads (say), we need to know that those laws hold for _all_ possible Monads (without laws, we don't really know anything about the methods of Monad - in a non-strict language, the methods might not even be well-defined for certain inputs). But Haskell doesn't even have a way to _state_ these laws formally, much less _prove_ them! I am working on a functional programming and specification language in my spare time which does have such formal methods features built-in, but it is not even implemented yet. (I can email you if I ever write a paper on it, but it may be some years before that happens.) However, there are various other angles which you can research: 1. Proofs as programs: _Constructive_ proofs of theorems can be automatically converted into programs in a functional programming language - although these programs are not always efficient. Indeed it is possible that a generated program will be far too inefficient to be useful. See for example "Proofs, Programs and Executable Specifications in Higher Order Logic", a Phd thesis by S Berghofer at http://www4.in.tum.de/~berghofe/papers/phd.pdf 1a. Models as functional programs: The very first sentence in Chapter 1 of the thesis I just cited, says: "Interactive theorem provers are tools which allow [one] to build abstract system models, often in some kind of functional programming language involving datatypes and recursive functions." 2. Dependent types: By programming in a dependently-typed functional programming language such as the research language Epigram, it is possible to write functional programs whose types force them to be correct. See for example "Why Dependent Types Matter" by Thorsten Altenkirch, Conor McBride, and James McKinna. However, in my opinion this is only useful for simple "sized types" such as "a list of length 6". For more complicated properties, I believe this approach is unnecessarily difficult, and does not match how mathematicians or programmers actually work. My approach (see above) clearly separates the programming, the theorems and the proofs, and (in principle) allows all three to be written in a fairly "natural" style. As opposed to dependent types which, in Epigram at least, seem to require threading proofs through programs (for some non-trivial proofs). 3. Separate formal methods tools for Haskell: My approach is to integrate formal methods directly into the essential core of a language, but this is quite unusual to say the least - a more normal thing to do (whether for functional or imperative languages) is prepare a separate formal methods tool for an existing programming language. This has been done for Haskell - see "Verifying haskell programs using constructive type theory" by Abel et. al. at http://portal.acm.org/citation.cfm?id=1088348.1088355 I have not considered testing in this email because another email already mentioned QuickCheck. -- Robin
Robin Green wrote:
2. Dependent types: By programming in a dependently-typed functional programming language such as the research language Epigram, it is possible to write functional programs whose types force them to be correct. See for example "Why Dependent Types Matter" by Thorsten Altenkirch, Conor McBride, and James McKinna. However, in my opinion this is only useful for simple "sized types" such as "a list of length 6". For more complicated properties, I believe this approach is unnecessarily difficult, and does not match how mathematicians or programmers actually work. My approach (see above) clearly separates the programming, the theorems and the proofs, and (in principle) allows all three to be written in a fairly "natural" style. As opposed to dependent types which, in Epigram at least, seem to require threading proofs through programs (for some non-trivial proofs).
I would just like to point out that there is nothing that forces you to "thread" the proofs through the programs. With dependent types you have this option, but you can also write standard "Haskell" code and have your proofs be separate. It's up to you to choose which way you do things. (If you do separate proofs you can even add some construct to the logic that makes it classical if you like.) Furthermore, I don't see such a clear separation between your points 1 and 2. With dependent types you are making proofs and then using them as programs. How much extraction you do is a matter of optimization, I'd say. And how efficient the extracted program is depends on which proof you choose to do. -- Lennart
Lennart Augustsson wrote:
Robin Green wrote:
2. Dependent types: By programming in a dependently-typed functional programming language such as the research language Epigram, it is possible to write functional programs whose types force them to be correct. See for example "Why Dependent Types Matter" by Thorsten Altenkirch, Conor McBride, and James McKinna. However, in my opinion this is only useful for simple "sized types" such as "a list of length 6". For more complicated properties, I believe this approach is unnecessarily difficult, and does not match how mathematicians or programmers actually work. My approach (see above) clearly separates the programming, the theorems and the proofs, and (in principle) allows all three to be written in a fairly "natural" style. As opposed to dependent types which, in Epigram at least, seem to require threading proofs through programs (for some non-trivial proofs).
I would just like to point out that there is nothing that forces you to "thread" the proofs through the programs. With dependent types you have this option, but you can also write standard "Haskell" code and have your proofs be separate.
But wouldn't that alternate way break the principle, recommended by Cardelli, that all code should be well-typed and the types of all terms should be, shall we say, "plainly" deducible from the code alone (i.e. not requiring any "difficult" reasoning on the part of the human reader)? If not, could you give an example to illustrate your point?
It's up to you to choose which way you do things. (If you do separate proofs you can even add some construct to the logic that makes it classical if you like.) Furthermore, I don't see such a clear separation between your points 1 and 2. With dependent types you are making proofs and then using them as programs. How much extraction you do is a matter of optimization, I'd say. And how efficient the extracted program is depends on which proof you choose to do.
Well I thought someone might say something like that - which is why I called them "angles" on the question. :) But while statements about types and statements about values might be inter-convertable, I think they look different and one can be more convenient than the other for various purposes. I've only used dependent types trivially so I could be wrong. -- Robin
I confess I haven't really been following this discussion, but a friend of mine has a recent paper that might be of interest (though it deals with ML rather than Haskell)... http://math.andrej.com/2005/04/09/specifications-via-realizability/ -- Hal Daume III | hdaume@isi.edu "Arrest this man, he talks in maths." | www.isi.edu/~hdaume
participants (6)
-
Abigail -
Hal Daume III -
Isaac Jones -
Jared Updike -
Lennart Augustsson -
Robin Green