I think one thing it means, is that, with the typesystem, you just can't do random things where-ever you want. Like, in the pure world if you want to transform values from one type to another, you always need to have implementations of functions available to do that. (You can't just take a pure value, get its mem location and interpret it as something else, without being explicid about it.) So when lining up your code (composing functions), you can be sure, that at least as far as types are concerned, everything is correct -- that such a program, that you wrote, can actually exist == that all the apropriate functions exist. And it is correct only that far -- the value-level coding is still up to you, so no mind-reading... -- Markus Läll On Fri, Feb 11, 2011 at 1:16 PM, Ivan Lazar Miljenovic < ivan.miljenovic@gmail.com> wrote:

On 11 February 2011 22:06, C K Kashyap wrote:

...

Hi Folks, I've come across this a few times - "In Haskell, once can prove the correctness of the code" - Is this true?

I'm not quite sure where you got that...

But since Haskell is pure, we can also do equational reasoning, etc. to help prove correctness. Admittedly, I don't know how many people actually do so...

...

I know that static typing and strong typing of Haskell eliminate a whole class of problems - is that related to the proving correctness? Is it about Quickcheck - if so, how is it different from having test sutites in projects using mainstream languages?

QuickCheck doesn't prove correctness: I had a bug that survived several releases tested regularly during development with a QC-based testsuite before it arose (as it required a specific condition to be satisfied for the bug to happen). As far as I know, a testsuite - no matter what language or what tools/methodologies are used - for a non-trivial piece of work just provides reasonable degree of assurance of correctness; after all, there could be a bug/problem you hadn't thought of!

-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com IvanMiljenovic.wordpress.com

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Am 11.02.2011 13:48, schrieb Daniel Fischer: [...] +1

Testing can only prove code incorrect, it can never prove code correct (except for extremely simple cases where testing all possible inputs can be done; but guaranteeing that QuickCheck generates all possible inputs is generally harder than a proof without testing in those cases).

Maybe smallcheck is better than QuickCheck for such (finite and simple) cases. http://hackage.haskell.org/package/smallcheck C.

On Sat, Feb 12, 2011 at 6:08 AM, C K Kashyap wrote:

Anyway, how can one go about explaining to an imperative programmer with no FP exposure - what aspect of Haskell makes it easy to refactor?

I think you just said it: typechecking, typechecking, typechecking. In Haskell, you can change one line of code and be confident that the compiler will force you to change every other line of code that's rendered nonsensical by your change. You just can't do that in C. It really liberates your mind and makes you less committed to your own design mistakes, since refactoring doesn't come with gut-wrenching worry that you'll introduce a silent error as a result. That said, I find that explaining Haskell's or ML's type system to someone used to a language with a much weaker type system is difficult. Many such people believe that type errors are trivial errors by definition and the compiler doesn't give them any help finding significant errors, which is true for the languages they've used (they may even believe that typecheckers get in their way by forcing them to correct errors). What's important is not just that Haskell has static typing, but that algebraic data types are a rich enough language to let you express your intent in data and not just in code. That helps you help the compiler help you. Cheers, Tim -- Tim Chevalier * http://cs.pdx.edu/~tjc/ * Often in error, never in doubt "an intelligent person fights for lost causes,realizing that others are merely effects" -- E.E. Cummings

On Sat, 12 Feb 2011 19:38:31 +0530 C K Kashyap wrote:

Anyway, how can one go about explaining to an imperative programmer with no FP exposure - what aspect of Haskell makes it easy to refactor?

Like other people have said, the static type system is a major factor. It's true that Haskell's type system is more advanced than most imperative languages but it's also the often not mentioned that static typing gives a stronger check in a functional language than an imperative ones even in simple cases. This is because all input and output data flow is type checked in a function application, whereas imperative side effects might escape checking. For example, the type signature for a variable swapping procedure in C: void swap(int *a, int *b) This will still type check even if it modified only one of the argument references. However, if written functionally, it must return a pair: swap :: (Int,Int) -> (Int,Int) Now the type checker will reject any implementation that fails to return a pair of results in every case. Of course for a trivial example like swap this is easy to ensure in any imperative language, but for more complex programs it is actually quite common to forget some update some component of the state. BTW, I found this and other interesting reflections on the avantages of FP vs. imperative in Martin Oderski's book "Programming in Scala". Best regards, Pedro Vasconcelos

On Mon, 14 Feb 2011 12:54:55 +0100 Tillmann Rendel wrote:

This benefit of explicit input and output values can interact nicely with parametric polymorphism:

swap :: (a, b) -> (b, a)

This more general type signature makes sure we are not just returning the input values unswapped.

Good point. This is a good reason why it's good practice to look for possiblity of writing more general functions and types even when they end up being used in a single instance. Pedro

On Mon, 14 Feb 2011 15:07:01 +0100 Gábor Lehel wrote:

I'm not completely sure, but I suspect another part of it (or maybe I'm just rephrasing what you said?) has to do with the fact that in Haskell, basically everything is an expression.

Yes, the fact that control statements (e.g. if-then-else) are expressions makes type checking much more effective. However, I think this is somewhat lost when programming imperative code in Haskell using a state or I/O monad (because a monadic type such as "IO t" does not discriminate what effects might take place, only the result type t). Of course one can use a more specialized monad (such ST for mutable references, etc.). I don't think that my imperative programs are automatically made more correct by writing them as monadic code in Haskell --- only that in Haskell I can opt for the functional style most of the time. BTW (slightly off topic) I found particularly annoying when teaching Python to be forced to use an imperative style (e.g. if-then-else are always statements). Scala is must better in this regard (altought it is not purely functional language); a statement is simply an expression whose return is unit. Pedro

Sorely, Haskell can't prove logic with it. No predicates on values, guarantee that proof is not _|_. Haskell makes bug free software affordable, that's true. But it's not a proof assistant. pavel On 14.02.2011, at 22:57, Albert Y. C. Lai wrote:

On 11-02-12 09:40 PM, Brandon S Allbery KF8NH wrote:

...

Only up to a point. While most of the responses so far focus on the question from one direction, the other is epitomized by a Knuth quote:

"Beware of bugs in the above code; I have only proved it correct, not tried it."

Knuth's definition of "proof" is of the sketchy kind of the mathematics community, not remotely close to the Coq kind. Even Dijsktra's and Bird's kind offers higher assurance than the traditional mathematician's sketchy kind.

There are still gaps, but drastically narrower than Knuth's gaps, and bridgeable with probability arbitrarily close to 1:

Possible defects in theorem provers: Use several theorem provers and/or several independent alternative implementations (both alternative software and alternative hardware).

Possible deviation of Haskell compilers from your assumed formal semantics of Haskell: Verify the compilers too, or modify the compilers to emit some sort of proof-carrying code.

Possible defects in target hardware: The hardware people are way ahead in improving both formal verification and manufacturing processes to reduce defects.

When John Harrison ( http://www.cl.cam.ac.uk/~jrh13/ ) has a proof for a floating-point algorithm, I would not dare to apply the Knuth quote on it.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Who claimed that Haskell is a proof assistant?

no one sanely will :) Haskell is a beautiful and practical (!) programming language with great infrastructure and community. Sadly, proving inside haskell is hard :) And it doesn't bring me coffee in the morning too (well, it mostly does) pavel. On 14.02.2011, at 23:08, Albert Y. C. Lai wrote:

On 11-02-14 03:03 PM, Pavel Perikov wrote:

...

Sorely, Haskell can't prove logic with it. No predicates on values, guarantee that proof is not _|_. Haskell makes bug free software affordable, that's true. But it's not a proof assistant.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe