Knuckledragger, a Semi-Automated Python Proof Assistant

This is my windmill tilting project. Pretty raw off the bench kind of stuff, but I'm interested to hear what kinds of things people would use this kind of thing for or ways to make this more understandable to an audience not soaked in formalism.

Nice write-up. If I find the time it would be interesting to dive a bit deeper than a shallow read and compare with how things are done in Rosette, which I have more experience with than the Z3Py-interface.<p><a href="https:&#x2F;&#x2F;docs.racket-lang.org&#x2F;rosette-guide&#x2F;index.html" rel="nofollow">https:&#x2F;&#x2F;docs.racket-lang.org&#x2F;rosette-guide&#x2F;index.html</a>

If you&#x27;ll pardon an extremely naive question:<p>Is this trying to prove things about Python code, or is it a Python interface to Z3, or something else?

How do your project and Z3 compare to (1) Logic programming tools like Prolog and (2) optimizers like scipy.optimize?<p>All of these seem to find solutions to user-provided constraint sets. They must be appropriate for different classes of problems, but it’s not obvious to me how that breaks out.<p>It’s, uh, been a long time since I last hand-rolled an optimization algorithm…