> I believe your argument on the performance penalty is right, and as a corollary, this implies that contracts are mostly useful if associated with a formal proof system. Contracts in production are probably a bad idea, in most cases.
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.
Honestly this does a better job of letting me know who is playing nearby than any other event advertising I've seen. I have no idea who these people are near me today, but now I get to sample and discover them. I actually just bought a ticket for a small show at a school near me that I never would have known of otherwise. I dunno if you're into making money off of this but it's the sort of idea that has some legs. Thanks!
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. :)
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.
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!
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:
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!
Portfolio of a slow but precise fuzzer + fast imprecise fuzzer is the easiest integration. Start both together and return the one which fails first. SMT solvers are often complementary with samplers.
However, it would be very interesting to see if a closer integration of symbolic and sampling methodologies is possible.
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!
This is a really minor nitpick that I am expressing to help you market this better. Instead of saying (defunct) PEP 316 just say inspired which communicates that you don’t do everything of pep 316 also .
Yes, please. I was confused when I first read this - I thought "why would I want to use a tool based on outdated syntax?". Maybe "PEP 316-inspired syntax"?
This is an area I'm trying to focus my Masters on, so any opportunity to apply what I'm reading is more than welcome! I'll add my email to my profile if you'd like to chat.
The README.md goes fast, but I have some feel for what's going on. Could I, for instance, connect a client and start logging every message in the system using a liberal matcher and a low weight?
Also, it's not obvious to me how the versions work. Can I use a transformer to "upgrade" an older message version to a newer one?
Yes, you could log every message by calling request.accept() with no criteria and applying a weight of -100, for example.
By default, only one instance of a processor (transformer) id is permitted - unless you mount additional versions. In "godsend-examples", there's an example named "versioning-processors". Selection of processor versions is determined in the profile of the user sending the request. In that example, in "users.json", the user "sender" is configured with any processor versions which ought to be substituted for that user. If there are multiple versions of a processor and none of those is indicated by the user sending the message, the processor version marked as the default, when it was mounted, will be run.
I'm glad that other folks think this is important too.
Stay tuned on twitter/medium. That python library also supports a viewabledict (for key-value mappings). I've got an experimental compiler which starts with an AST (stored as a tree of these maps), and then chains type checking and code generation off that to make incrementally updating binaries. Just supporting a toy language to start, but it will make a nice demo I think!
That's great. Why aren't all compilers like that? How comes in visual studio for instance you can have a build that takes a minute, but linting and verification tools that react immediately to code changes. I think we're being short changed!
This is exciting because (1) it suggests the equivalent transformation for sided reduces (folds), and (2) fold is a more general operator than the others. My somewhat silly use of "hypothetical inverses" effectively just creates a goalpost to (1) constructively find the the function f, given g (or vice-versa) and (2) prove the necessary condition.
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.