3 ms·

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 examp

by 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.

by rtpg 2y ago

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.