Hacker News Reader

Comment by mbid | Hacker News Reader

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?

View on HN

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-ha...

https://code.facebook.com/posts/745068642270222/fighting-spa...

I don't think a spam filter would be the first thing you'd prove correct if you wanted to go down that road..

> 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.

> 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.

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.

> 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?

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.

> 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.

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

Well you can't use this approach to verify haskell code if you don't know coq.

But you can write a library in Haskell, verify it with Coq, and publish it on Hackage for everybody to benefit from.

Indeed, and reading Coq errors should be a lot easier than having to work out how to write a Coq program.

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

Reply on news.ycombinator.com