8 ms·

Finding bugs in Haskell code by proving it

205 points by based2 9y ago

of 9y ago
What the hell - i already submitted this here: https://news.ycombinator.com/item?id=15875970 https://news.ycombinator.com/item?id=15875970 Anyways, this is a great article, and I love the background!
romeo88 9y ago
slept away while reading it
- cryptocat 9y ago
  me too, lol
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.
lcdoutlet 9y ago
Nice Post! I think tools that enable formal reasoning about code are incredibly valuable. Just going through the process the author was able to find and fix three bugs. Could you imagine a pipeline where people submitted code that had already been proven to be correct? Sounds amazing!
tomsmeding 9y ago
This looks really cool! I've never worked with Coq myself, and really, the process described here still looks much too convoluted for practically proving nontrivial amounts of code correct. But it looks like lots of fun too! And it is sort-of the holy grail of computer science, writing code and being able to prove it correct instead of just testing it with maybe-or-maybe-not enough test cases. In practice I find that Haskell itself already prevents a lot of bugs, but of course in functions like the one dissected here, logical errors are still easily made. I'll definitely look into Coq one of these weeks.
- lcdoutlet 9y ago
  http://www.cl.cam.ac.uk/~jrh13/hol-light/ http://www.cl.cam.ac.uk/~jrh13/hol-light/ The author John Harrison who works at Intel has used his theorem proving application hol-light in doing verification on large code bases.
- neilparikh 9y ago
  You might already know about this, but if you're looking to learn Coq, I would recommend the Software Foundations series (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/).
  - harveywi 9y ago
    I started with Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/). If you are more interested in programming, consider trying Idris (http://idris-lang.org/ http://idris-lang.org/). Edwin Brady, the language designer, wrote a great book that I would recommend called Type-Driven Development with Idris (https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...).
- nickpsecurity 9y ago
  I have a stock recommendation for this if you want to learn formal methods to hopefully prove some useful programs. It might also apply if you want to do it for fun but don't want to get weighed down too much. https://news.ycombinator.com/item?id=15781508 https://news.ycombinator.com/item?id=15781508
based2 9y ago
https://www.reddit.com/r/programming/comments/7iuakc/finding_bugs_in_haskell_code_by_proving_it/ https://www.reddit.com/r/programming/comments/7iuakc/finding...
namuol 9y ago
Mostly-off-topic: The `bisect-binary` project listed in the introduction is almost the _exact_ program I made while I was a devious high school student trying to circumvent weak (i.e. most widely-used-) antivirus software by locating a few "key" bytes in the binary that the AV used to fingerprint a virus. I would zero out half the file, scan the file with AV, then recursively repeat the same for any zero'd regions of files that AV didn't consider a virus. Essentially a search of the file for the smallest set of bytes that needed to be changed for AV to fail detection. Usually this would result in only a small number of bytes that needed to be slightly tweaked. Pretty unproductive "hobby", but I must admit it was really fun. :)
- maweki 9y ago
  This sounds fun. How did you handle the case where on a bisect both halves didn't trigger the AV on their own?
  - namuol 9y ago
    This was pretty rare for the most popular AVs, but if it didn't work I would try manually zeroing different sections until I found something. I was surprised how easy it was to make a virus undetected, and that they didn't routinely change their fingerprint algorithm as a defense against this attack.
thethirdone 9y ago
I have been playing around with an idea for a programming language that enables practical theorem proving. The core idea behind it is that statically proven assertions would be really powerful. Loop invariants can be simply expressed as an assertion inside the loop. Additionally, to give it a bit more power; assertions could be given the ability to act over sets (say over all ints). This might look something like XY = {int, int} @assert commutative fn add(a XY, b XY) XY { return (a[0]+b[0], a[1] + b[1]) } fn commutative<a,b>(f (a,a)b){ assert x,y: f(x,y) == f(y,x) } And then it would also be helpful to add on assertions to types so assignments to variables also checks the assertions order = enum {greater, equal, lesser} comparator<a> = (a,a)order fn sorted<a>(pair ([]a,comparator<a>))bool { (l, cmp) = pair if l.length() <= 1 { return true } return cmp(l[0],l[1]) != order.greater & sorted((l[1:],cmp)) } SortedList<a> = ([]a,(a,a)order) & sorted There are a few major issues with my idea currently (it really requires dependent types to be ergonomic and allocation and pointers could be strange) which have prevented me from making a quick demo compiler or language spec. But I would be very excited to discuss it.
- PeCaN 9y ago
  Reminds me a lot of LiquidHaskell, you should take a look at what they've done if you haven't seen it yet. It's a very good idea IMO. https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
- ghkbrew 9y ago
  Have you looked into research regarding refinement types? Because they describe almost exactly what your reaching for (types with assciated provable assertions). Specifically Liquid Haskell[0] extends Haskell with (dependent) refinement types, but keeps the type checking decidable and the proof burden relatively light by using a restricted predicate language and an SMT solver. [0] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
  - thethirdone 9y ago
    Yeah, I am aware of refinement types. You can do a lot of what I am envisioning with just refinement types. Expressing loop invariants with just refinement types is really awkward though. The main reason why the language I am envisioning is not a functional language is because Idris, Liquid haskell, ... have already explored many of the related ideas. I want to take ideas from them and bring it into an imperative language as that hasn't been as well explored.
techupcian 9y ago
I was experiencing some bugs and more difficulties while I’m on my computer Cos of my Company website and this legitimate hackerdanielssmith@gmail.com has come to be of great help to me and I can assure you of a successful job when you contact the email .

205 points by based2 9y ago

of 9y ago

What the hell - i already submitted this here: https://news.ycombinator.com/item?id=15875970 https://news.ycombinator.com/item?id=15875970 Anyways, this is a great article, and I love the background!

romeo88 9y ago

slept away while reading it

cryptocat 9y ago
me too, lol

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.

lcdoutlet 9y ago

Nice Post! I think tools that enable formal reasoning about code are incredibly valuable. Just going through the process the author was able to find and fix three bugs. Could you imagine a pipeline where people submitted code that had already been proven to be correct? Sounds amazing!

tomsmeding 9y ago

This looks really cool! I've never worked with Coq myself, and really, the process described here still looks much too convoluted for practically proving nontrivial amounts of code correct. But it looks like lots of fun too! And it is sort-of the holy grail of computer science, writing code and being able to prove it correct instead of just testing it with maybe-or-maybe-not enough test cases. In practice I find that Haskell itself already prevents a lot of bugs, but of course in functions like the one dissected here, logical errors are still easily made. I'll definitely look into Coq one of these weeks.

lcdoutlet 9y ago
http://www.cl.cam.ac.uk/~jrh13/hol-light/ http://www.cl.cam.ac.uk/~jrh13/hol-light/ The author John Harrison who works at Intel has used his theorem proving application hol-light in doing verification on large code bases.
neilparikh 9y ago
You might already know about this, but if you're looking to learn Coq, I would recommend the Software Foundations series (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/).
- harveywi 9y ago
  I started with Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/). If you are more interested in programming, consider trying Idris (http://idris-lang.org/ http://idris-lang.org/). Edwin Brady, the language designer, wrote a great book that I would recommend called Type-Driven Development with Idris (https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...).
nickpsecurity 9y ago
I have a stock recommendation for this if you want to learn formal methods to hopefully prove some useful programs. It might also apply if you want to do it for fun but don't want to get weighed down too much. https://news.ycombinator.com/item?id=15781508 https://news.ycombinator.com/item?id=15781508

based2 9y ago

https://www.reddit.com/r/programming/comments/7iuakc/finding_bugs_in_haskell_code_by_proving_it/ https://www.reddit.com/r/programming/comments/7iuakc/finding...

namuol 9y ago

Mostly-off-topic: The `bisect-binary` project listed in the introduction is almost the _exact_ program I made while I was a devious high school student trying to circumvent weak (i.e. most widely-used-) antivirus software by locating a few "key" bytes in the binary that the AV used to fingerprint a virus. I would zero out half the file, scan the file with AV, then recursively repeat the same for any zero'd regions of files that AV didn't consider a virus. Essentially a search of the file for the smallest set of bytes that needed to be changed for AV to fail detection. Usually this would result in only a small number of bytes that needed to be slightly tweaked. Pretty unproductive "hobby", but I must admit it was really fun. :)

maweki 9y ago
This sounds fun. How did you handle the case where on a bisect both halves didn't trigger the AV on their own?
- namuol 9y ago
  This was pretty rare for the most popular AVs, but if it didn't work I would try manually zeroing different sections until I found something. I was surprised how easy it was to make a virus undetected, and that they didn't routinely change their fingerprint algorithm as a defense against this attack.

thethirdone 9y ago

I have been playing around with an idea for a programming language that enables practical theorem proving. The core idea behind it is that statically proven assertions would be really powerful. Loop invariants can be simply expressed as an assertion inside the loop. Additionally, to give it a bit more power; assertions could be given the ability to act over sets (say over all ints). This might look something like XY = {int, int} @assert commutative fn add(a XY, b XY) XY { return (a[0]+b[0], a[1] + b[1]) } fn commutative<a,b>(f (a,a)b){ assert x,y: f(x,y) == f(y,x) } And then it would also be helpful to add on assertions to types so assignments to variables also checks the assertions order = enum {greater, equal, lesser} comparator<a> = (a,a)order fn sorted<a>(pair ([]a,comparator<a>))bool { (l, cmp) = pair if l.length() <= 1 { return true } return cmp(l[0],l[1]) != order.greater & sorted((l[1:],cmp)) } SortedList<a> = ([]a,(a,a)order) & sorted There are a few major issues with my idea currently (it really requires dependent types to be ergonomic and allocation and pointers could be strange) which have prevented me from making a quick demo compiler or language spec. But I would be very excited to discuss it.

PeCaN 9y ago
Reminds me a lot of LiquidHaskell, you should take a look at what they've done if you haven't seen it yet. It's a very good idea IMO. https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
ghkbrew 9y ago
Have you looked into research regarding refinement types? Because they describe almost exactly what your reaching for (types with assciated provable assertions). Specifically Liquid Haskell[0] extends Haskell with (dependent) refinement types, but keeps the type checking decidable and the proof burden relatively light by using a restricted predicate language and an SMT solver. [0] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
- thethirdone 9y ago
  Yeah, I am aware of refinement types. You can do a lot of what I am envisioning with just refinement types. Expressing loop invariants with just refinement types is really awkward though. The main reason why the language I am envisioning is not a functional language is because Idris, Liquid haskell, ... have already explored many of the related ideas. I want to take ideas from them and bring it into an imperative language as that hasn't been as well explored.

techupcian 9y ago

I was experiencing some bugs and more difficulties while I’m on my computer Cos of my Company website and this legitimate hackerdanielssmith@gmail.com has come to be of great help to me and I can assure you of a successful job when you contact the email .