Timeline for Can this set of propositions be represented and proved in Haskell?
Current License: CC BY-SA 4.0
10 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Jan 24, 2019 at 19:29 | comment | added | Patrick Browne | A previous question helped me to distinguish between a constructive proof and a program. | |
Jan 23, 2019 at 7:19 | comment | added | Andrej Bauer | @PatrickBrowne: I am not impressed by that paper. They are confused by the word "constructive". The statement $\exists y . y^2 = x$ has a constructive proof, but they claim it is non-constructive. They do not seem to know the difference between "constructive" and "has an operational semantics". They do not address the fact that Haskell only supports expression of very specific equations that are executable (for instance, they cannot express something as simple as commutativity). The baby examples are just an intro to Haskell programming, far from anything realistic. And so on. | |
Dec 23, 2018 at 12:21 | comment | added | Patrick Browne | Frank and Medak consider Haskell equations as constructive axioms. | |
Dec 23, 2018 at 11:08 | comment | added | Patrick Browne | In particular I have difficulty in understanding Werner Kuhn's approach to Haskell see an earlier question. | |
Dec 23, 2018 at 10:34 | comment | added | Patrick Browne | Not sure. More statements I am unsure of: Axioms expressed in Haskell, types as theories, I do understand Goguen's version, Haskell as an algebraic specification language and prove the correctness | |
Dec 22, 2018 at 21:56 | comment | added | Andrej Bauer | What does "Haskell can represent theories that can be proved" mean? And who are these mysterious researchers? | |
Dec 22, 2018 at 11:03 | vote | accept | Patrick Browne | ||
Dec 22, 2018 at 11:01 | comment | added | Patrick Browne | I am aware of the type level reasoning and the role of Prolog and I completely agree with your comments. There is a body of researchers who have made what I believe to be exaggerated claims about Haskell, claiming that Haskell can represent theories that can be proved. My posts are attempts to look for any evidence of these claims. | |
Dec 22, 2018 at 10:53 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 126 characters in body
|
Dec 22, 2018 at 10:48 | history | answered | Andrej Bauer | CC BY-SA 4.0 |