Skip to main content
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