pschanely
Joined 14 years ago
Karma
167
Submissions
48
Member since
Oct 25
Recent submissions
Comment · 2 years ago
Comment · 3 years ago
A little encouragement goes such a long way. Thank you for trying it out, and especially for coming back here to let me know how it went!
Comment · 3 years ago
Oh, thank you! I don't have any plans for expanding to other music services. But skimming the Apple Music API, I think it's possible. Particularly if you think you'd use it, I'll investigate a bit more and let you know. :)
Comment · 3 years ago
Music Tonight: https://musictonightapp.com/
Makes a Spotify playlist of artists playing near you, tonight.
No revenue. I really just made it for me; make the playlist in the am, listen during the day, and maybe see something that night.
Comment · 5 years ago
Great! Sadly, I don't see anything on linkedin though. Feel free to just ping me by email: [email protected]
Comment · 5 years ago
Sadly, mine largely aren't committed to words yet. I do have a small thing on implementing regular expressions: https://medium.com/@pschanely/modeling-python-regular-expres...
But there is so much to talk about: gotchas with quantifiers, mixing logics, multiplication, float conversions. I'll try to write up some more of my experiences if that's valuable for folks!
Comment · 5 years ago
Looking at some of your SMT-based projects, I'd love to compare your SMT solver notes with my mine from working on https://github.com/pschanely/CrossHair
Sadly, there aren't a lot of resources on how to use SMT solvers well.
Comment · 6 years ago
Totally agree that this is confusing. I've stolen and committed your suggestion. Thank you both!
Comment · 6 years ago
Yes. Z3 is impressive. I intend to do a write-up of how I chose to model Python values in it soon.
Comment · 6 years ago
That's right! We pick different choose execution paths arbitrarily and accumulate constraints in an SMT solver as we go. It's implemented with special objects that look just like ints, strings, etc; this might help:
Comment · 6 years ago
That would be amazing. It's easy to turn CrossHair into an absurdly slow fuzz tester (imagine hashing or printing your inputs early in the process). I think the ideal product would be good at both symbolic and concrete tactics, and the minimization logic of hypothesis would be really nice to have too.
I will be in touch!
Comment · 6 years ago
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!
Agree! There is a sliding scale between testing contracts and proving them too. My labor of love for the past several years has been a tool for checking Python contracts using an SMT solver (using symbolic inputs over concrete paths): https://github.com/pschanely/CrossHair
That said, these days I think property-based testing gets you the ~same benefits as contracts, and is easier for most people to apply.