40 ms·

I have trouble understanding the usefulness of this. Haskell is barely used in the first place, and even less for highly safety critical software. It's also no

by mbid 9y ago

I have trouble understanding the usefulness of this. Haskell is barely used in the first place, and even less for highly safety critical software. It's also not clear to me why I would use this over writing the program in the constructive logic of coq, agda or idris and then extract ("compile") the program from the proof itself. Of course, a usecase would be to formally verify "legacy" haskell code, but then my first point applies -- there is not that much important haskell code out there. The last reason for the existence of this program I could see is that this is just experimental and the authors want to explore whether it's possible to formally prove things about haskell programs. But isn't that obviously true, given enough time put into the project?

deleted 9y ago
[deleted]
viraptor 9y ago
> there is not that much important haskell code out there. In other words, there's at least some important Haskell code, and there's Haskell code important to someone. That's a good enough reason. Or are you saying we can't have nice things?
- mbid 9y ago
  Well, I assume this is at least partially funded by the public. Most side projects are not. While I appreciate that the engineering that went into this is non-trivial, I fail to see the scientific relevance.
nl 9y ago
A lot more people know Haskell than know Coq, so there's that.
- mbid 9y ago
  Well you can't use this approach to verify haskell code if you don't know coq.
  - chongli 9y ago
    But you can write a library in Haskell, verify it with Coq, and publish it on Hackage for everybody to benefit from.
    - nl 9y ago
      Indeed, and reading Coq errors should be a lot easier than having to work out how to write a Coq program.
samgd 9y ago
Standard Chartered has over 3 million lines of Haskell code and Facebook uses it to fight spam - there's definitely more than you think out there :-) http://hauptwerk.blogspot.co.uk/2017/04/four-openings-for-haskell-developers-at.html http://hauptwerk.blogspot.co.uk/2017/04/four-openings-for-ha... https://code.facebook.com/posts/745068642270222/fighting-spam-with-haskell/ https://code.facebook.com/posts/745068642270222/fighting-spa...
- mbid 9y ago
  I don't think a spam filter would be the first thing you'd prove correct if you wanted to go down that road..
- virtualwhys 9y ago
  > Standard Chartered has over 3 million lines of Haskell code Not exactly, they have their own closed source fork of GHC, which is strictly evaluated. Given that the codebase is proprietary it's unknown what other differences there are beyond having dumped lazy evaluation. It's a Haskell-like language, but far different than the Haskell that the public has access to.
thinkpad20 9y ago
> I have trouble understanding the usefulness of this. Well for one thing, sometimes projects are just for fun, or to explore uncharted territory, without thinking about a specific use case. For another, there are definitely use cases for proofs in code, as verified software appears in a variety of domains. It’s not likely to make its way into the average CRUD app any time soon, but that doesn’t mean it’s not useful. > Haskell is barely used in the first place, and even less for highly safety critical software. “Barely used” is relative. Compared to java or python, sure. But there are untold millions of lines of Haskell code running in production right now. Besides, in my humble opinion Haskell should be used more, whether or not it is (right now). And in any case Haskell has had a big influence on many other more popular languages, and/or libraries, and this could one day be another example of that.
- mbid 9y ago
  This is not (just) for fun: "But things have changed since then, as a group at UPenn (mostly Antal Spector-Zabusky, Stephanie Weirich and myself) has created hs-to-coq: a translator from Haskell to the theorem prover Coq." I agree that haskell should be used more, at least if the alternative is one of the main stream languages.
dozzie 9y ago
> I have trouble understanding the usefulness of this. Haskell is barely used in the first place, and even less for highly safety critical software. Every new approach is initially barely used in the wild, and the initial method of such a new approach is usually quite different in details from how things end up eventually. In this case the value lies in working out how proving software could look like, and proving program after writing it is a different direction than writing it to a proof. We can't tell which of these methods is more useful or convenient before somebody checks them out.
nine_k 9y ago
Consider it a step to a more general approach. Maybe some parts will be useful. Imagine applying this to Rust and Scala.

by mbid 9y ago

deleted 9y ago

[deleted]

viraptor 9y ago

> there is not that much important haskell code out there. In other words, there's at least some important Haskell code, and there's Haskell code important to someone. That's a good enough reason. Or are you saying we can't have nice things?

mbid 9y ago
Well, I assume this is at least partially funded by the public. Most side projects are not. While I appreciate that the engineering that went into this is non-trivial, I fail to see the scientific relevance.

nl 9y ago

A lot more people know Haskell than know Coq, so there's that.

mbid 9y ago
Well you can't use this approach to verify haskell code if you don't know coq.
- chongli 9y ago
  But you can write a library in Haskell, verify it with Coq, and publish it on Hackage for everybody to benefit from.
  - nl 9y ago
    Indeed, and reading Coq errors should be a lot easier than having to work out how to write a Coq program.

samgd 9y ago

Standard Chartered has over 3 million lines of Haskell code and Facebook uses it to fight spam - there's definitely more than you think out there :-) http://hauptwerk.blogspot.co.uk/2017/04/four-openings-for-haskell-developers-at.html http://hauptwerk.blogspot.co.uk/2017/04/four-openings-for-ha... https://code.facebook.com/posts/745068642270222/fighting-spam-with-haskell/ https://code.facebook.com/posts/745068642270222/fighting-spa...

mbid 9y ago
I don't think a spam filter would be the first thing you'd prove correct if you wanted to go down that road..
virtualwhys 9y ago
> Standard Chartered has over 3 million lines of Haskell code Not exactly, they have their own closed source fork of GHC, which is strictly evaluated. Given that the codebase is proprietary it's unknown what other differences there are beyond having dumped lazy evaluation. It's a Haskell-like language, but far different than the Haskell that the public has access to.

thinkpad20 9y ago

> I have trouble understanding the usefulness of this. Well for one thing, sometimes projects are just for fun, or to explore uncharted territory, without thinking about a specific use case. For another, there are definitely use cases for proofs in code, as verified software appears in a variety of domains. It’s not likely to make its way into the average CRUD app any time soon, but that doesn’t mean it’s not useful. > Haskell is barely used in the first place, and even less for highly safety critical software. “Barely used” is relative. Compared to java or python, sure. But there are untold millions of lines of Haskell code running in production right now. Besides, in my humble opinion Haskell should be used more, whether or not it is (right now). And in any case Haskell has had a big influence on many other more popular languages, and/or libraries, and this could one day be another example of that.

mbid 9y ago
This is not (just) for fun: "But things have changed since then, as a group at UPenn (mostly Antal Spector-Zabusky, Stephanie Weirich and myself) has created hs-to-coq: a translator from Haskell to the theorem prover Coq." I agree that haskell should be used more, at least if the alternative is one of the main stream languages.

dozzie 9y ago

> I have trouble understanding the usefulness of this. Haskell is barely used in the first place, and even less for highly safety critical software. Every new approach is initially barely used in the wild, and the initial method of such a new approach is usually quite different in details from how things end up eventually. In this case the value lies in working out how proving software could look like, and proving program after writing it is a different direction than writing it to a proof. We can't tell which of these methods is more useful or convenient before somebody checks them out.

nine_k 9y ago

Consider it a step to a more general approach. Maybe some parts will be useful. Imagine applying this to Rust and Scala.