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]
http://www.cs.kent.ac.uk/pubs/1995/6
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 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 tota
> 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 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?
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 w
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 o
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-t
On Mon, Feb 14, 2011 at 12:06 PM, Pedro Vasconcelos wrote:
> 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
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 unswapp
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 ty
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
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 ha
-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, th
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 li
>
> 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 lo
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
On Fri, Feb 11, 2011 at 4:06 AM, 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?
You can prove the correctness of code for any language that has
precise semantics. Which is basically none of them (I b
On Fri, Feb 11, 2011 at 3:06 AM, 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 know that static typing and strong typing of Haskell eliminate a whole
> class of problems - is that related to
Kashyap,
2011/2/11 C K Kashyap :
> 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 abo
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 harde
>
> 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 transf
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 t
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 prop
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 val
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 c
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
27 matches
Mail list logo