I did some work years ago about giving a predicate logic treatment of Haskell,
based on earlier work for Miranda, and formalised some proofs based on this in
Isabelle. Here are the links:
Logic for Miranda, revisited [from Formal Aspects of Computing, 1995]
On Sat, 12 Feb 2011 19:38:31 +0530
C K Kashyap ckkash...@gmail.com 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
Pedro Vasconcelos wrote:
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
On Mon, 14 Feb 2011 12:54:55 +0100
Tillmann Rendel ren...@informatik.uni-marburg.de 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
On Mon, Feb 14, 2011 at 12:06 PM, Pedro Vasconcelos p...@dcc.fc.up.pt wrote:
On Sat, 12 Feb 2011 19:38:31 +0530
C K Kashyap ckkash...@gmail.com 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?
On Mon, 14 Feb 2011 15:07:01 +0100
Gábor Lehel illiss...@gmail.com 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
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
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
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.
Who claimed that Haskell is a proof assistant?
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)
On 14.02.2011, at 03:03 PM, Pavel Perikov [peri...@gmail.com] 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.
Being equivalent to a class of
On 2/11/11 1:25 PM, Luke Palmer wrote:
I would like to see a language
that allowed optional verification, but that is a hard balance to make
because of the interaction of non-termination and the evaluation that
needs to happen when verifying a proof.
I believe that ATS (short for Advanced Type
On 2/12/11 11:41 AM, Tim Chevalier wrote:
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.
ADTs are an amazing thing to
Ivan Lazar Miljenovic wrote:
C K Kashyap wrote:
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.
many of the subtleties encountered in the process. I am often 100%
sure of the correctness of my refactors.
While I have an intuitive understanding of what you mean about the
correctness of refactoring ... I personally feel much more comfortable
refactoring Haskell code ... as in - as long
On Sat, Feb 12, 2011 at 6:08 AM, C K Kashyap ckkash...@gmail.com 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
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 2/11/11 06:06 , C K Kashyap wrote:
I've come across this a few times - In Haskell, once can prove the
correctness of the code - Is this true?
Only up to a point. While most of the responses so far focus on the
question from one direction, the
Hi Folks,
I've come across this a few times - In Haskell, once can prove the
correctness of the code - Is this true?
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
On 11 February 2011 22:06, C K Kashyap ckkash...@gmail.com 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.
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
On 02/11/2011 12:06 PM, C K Kashyap wrote:
[...]
I know that static typing and strong typing of Haskell eliminate a
whole class of problems - is that related to the proving correctness?
[...]
You might have read about free theorems arising from types. They are a
method to derive certain
On Friday 11 February 2011 12:06:58, 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?
One can also prove the correctness of the code in other languages.
What makes these proofs much easier in Haskell than
I've come across this a few times - In Haskell, once can prove the
correctness of the code - Is this true?
One way to prove the correctness of a program is to calculate it from its
specification. If the specification is also a Haskell program, equational
reasoning can be used to transform a
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
Kashyap,
2011/2/11 C K Kashyap ckkash...@gmail.com:
I've come across this a few times - In Haskell, once can prove the
correctness of the code - Is this true?
I know that static typing and strong typing of Haskell eliminate a whole
class of problems - is that related to the proving
On Fri, Feb 11, 2011 at 3:06 AM, C K Kashyap ckkash...@gmail.com 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 know that static typing and strong typing of Haskell eliminate a whole
class of problems - is that
On Fri, Feb 11, 2011 at 4:06 AM, C K Kashyap ckkash...@gmail.com wrote:
Hi Folks,
I've come across this a few times - In Haskell, once can prove the
correctness of the code - Is this true?
You can prove the correctness of code for any language that has
precise semantics. Which is basically
27 matches
Mail list logo
