from Hacker News

Show HN: CrossHair – SMT Assisted Testing for Python

by pschanely on 1/15/20, 2:35 PM with 14 comments

• by ZeroCool2u on 1/15/20, 5:00 PM

  Hey there, this project looks really great! There seems to be some overlap with the Hypothesis-Auto[1] project. Have you looked into collaborating with Tim and perhaps merging your work together? It seems like it would be very powerful!

  [1] https://timothycrosley.github.io/hypothesis-auto/

• by pschanely on 1/15/20, 2:35 PM

  Hi all! My primary objective with this post is to find potential collaborators and people willing to try it. (and file bugs!)

  If you do try it, I'd encourage you to think of it as an exercise in formally documenting your code's behavior, with the side benefit that CrossHair can sometimes help you ensure the correctness of that documentation.

  And, of course, feedback of any kind at all is honestly appreciated. Thanks for being the awesome community that you are!

• by philzook on 1/15/20, 8:53 PM

  Very cool! Ever looked at the Viper project? It's the only other system in python that I know of targeting pre and post conditions

  https://www.pm.inf.ethz.ch/research/viper.html

  https://www.pm.inf.ethz.ch/research/nagini.html

  Another thing that might be of interest is HOLpy. I have no idea what the state of that is. https://arxiv.org/abs/1905.05970

  I was fiddling around recently with way jankier methods than what you've done here http://www.philipzucker.com/programming-and-interactive-prov...

• by typon on 1/15/20, 5:30 PM

  This looks really cool. Love to see z3 being used for tools.

• by im_down_w_otp on 1/15/20, 5:05 PM

  So this is Symbolic Execution based testing for Python?