5 ms·

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

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.

rtpg 2y ago
Is there an idea here that you could write out a script and then compile out a Python implementation (for example?), given you have the `Record` code, for example? I have had a decent number of times where if I was told "write this code in this Python DSL, and then you can do interactive theorem proofs just on that bit", I would be pretty satisfied, even if it meant really cutting down what kind of objects I could use in the process.
- philzook 2y ago
  I think what you're referring to is code generation or extraction https://coq.inria.fr/doc/V8.11.1/refman/addendum/extraction.html https://coq.inria.fr/doc/V8.11.1/refman/addendum/extraction.... out of knuckledragger? It wouldn't be that difficult to traverse a z3 expression and generate the text of reasonable python code for a subset of possible z3 expressions. It would probably be easiest to extract purely functional code, which would be somewhat non-idiomatic python. I suppose extraction to pytorch, numpy, or pandas could be useful. If by "Record" you're referring to the Record helper in the blog post, that was nothing clever. Just a helper to define struct-like datatypes (record types). I did do some experimentation using the python parser to turn python code into z3 expressions but I haven't pushed on that https://www.philipzucker.com/applicative_python/ https://www.philipzucker.com/applicative_python/ It is a little annoying to not be able to use the nice native python if-then-else or match syntax.
  - rtpg 2y ago
    Bit of a different space, but Amaranth does some fun stuff to copy control flow. It's obviously not "native" `if-then-else` but it's close enough for things that matter IMO. https://amaranth-lang.org/docs/amaranth/latest/guide.html#control-flow https://amaranth-lang.org/docs/amaranth/latest/guide.html#co...
    - philzook 2y ago
      Very interesting.

rtpg 2y ago

Is there an idea here that you could write out a script and then compile out a Python implementation (for example?), given you have the `Record` code, for example? I have had a decent number of times where if I was told "write this code in this Python DSL, and then you can do interactive theorem proofs just on that bit", I would be pretty satisfied, even if it meant really cutting down what kind of objects I could use in the process.

philzook 2y ago
I think what you're referring to is code generation or extraction https://coq.inria.fr/doc/V8.11.1/refman/addendum/extraction.html https://coq.inria.fr/doc/V8.11.1/refman/addendum/extraction.... out of knuckledragger? It wouldn't be that difficult to traverse a z3 expression and generate the text of reasonable python code for a subset of possible z3 expressions. It would probably be easiest to extract purely functional code, which would be somewhat non-idiomatic python. I suppose extraction to pytorch, numpy, or pandas could be useful. If by "Record" you're referring to the Record helper in the blog post, that was nothing clever. Just a helper to define struct-like datatypes (record types). I did do some experimentation using the python parser to turn python code into z3 expressions but I haven't pushed on that https://www.philipzucker.com/applicative_python/ https://www.philipzucker.com/applicative_python/ It is a little annoying to not be able to use the nice native python if-then-else or match syntax.
- rtpg 2y ago
  Bit of a different space, but Amaranth does some fun stuff to copy control flow. It's obviously not "native" `if-then-else` but it's close enough for things that matter IMO. https://amaranth-lang.org/docs/amaranth/latest/guide.html#control-flow https://amaranth-lang.org/docs/amaranth/latest/guide.html#co...
  - philzook 2y ago
    Very interesting.