[HN Gopher] Knuckledragger, a Semi-Automated Python Proof Assistant
___________________________________________________________________
Knuckledragger, a Semi-Automated Python Proof Assistant
Author : philzook
Score : 49 points
Date : 2024-08-05 14:02 UTC (8 hours ago)
(HTM) web link (www.philipzucker.com)
(TXT) w3m dump (www.philipzucker.com)
| philzook wrote:
| 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.
| nanolith wrote:
| Nice work.
|
| Some things that I think work well for SMT solvers:
|
| 1. Bounded model checking for source code.
|
| 2. Finding solutions to constraint problems.
|
| 3. Design rule checking for hardware layout and logic gates.
|
| Recently, I built a simple scheduling system using Z3. My wife
| is a librarian supervisor, and she's been spending hours each
| week creating schedules by hand. But, with a little Z3, one can
| enumerate the constraints and let it find a viable example. If
| the example doesn't work, add more constraints until it does.
| philzook wrote:
| Z3 is a marvel. Even if this project is of no interest to a
| person, Z3 might be. I have intentionally, literally, used z3
| data structures to make that transition easier should one
| find something intriguing here over top of what z3 offers.
| CoastalCoder wrote:
| How very cool!
|
| Can you give an example of the kinds of constraints that need
| to get tweaked?
|
| And do you have to tweak them in Z3 each time?
|
| Disclaimer: I know almost nothing about Z3. I'm just
| picturing you trying to convince her that something like
| datalog has a learning curve that she'll Totally Be Glad she
| Powered Through, and she'll Thank you Later for Talking he
| Into It :)
| 0cf8612b2e1e wrote:
| I have used z3 for a job scheduling problem. I had a piece of
| equipment which can handle capacity X, jobs come in at known
| intervals and are available for given durations of varying
| lengths, some jobs come in multiple times, some jobs must be
| done above all others. Which jobs should be assigned to the
| equipment to maximize completed jobs while not missing the high
| priority entries?
|
| Numbers were such that you could only ever handle a fraction of
| the possible work. The throughout of a good allocation could be
| significantly higher than a naive one.
| CoastalCoder wrote:
| If you'll pardon an extremely naive question:
|
| Is this trying to prove things about Python code, or is it a
| Python interface to Z3, or something else?
| philzook wrote:
| Not naive.
|
| It is not trying to prove things about python code.
|
| It is building facilities and theory libraries around the pre-
| existing z3 python interface in a manner that can be reasonably
| called an interactive theorem prover. Hopefully, eventually,
| with a lower barrier to entry (and probably lower expressivity
| ceiling) than pre-existing systems like Lean, Coq, Isabelle.
|
| I am targeting applications close to my heart, like calculus,
| differential equations, dynamical systems, numerical
| calculations, software verification. It is a tall order. No
| promises.
| cess11 wrote:
| 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.
|
| https://docs.racket-lang.org/rosette-guide/index.html
___________________________________________________________________
(page generated 2024-08-05 23:00 UTC)