undefined | Better HN

0 pointsrtpg1y ago0 comments

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.

0 comments

3 comments · 1 top-level

philzook1y ago· 2 in thread

I think what you're referring to is code generation or extraction 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/ It is a little annoying to not be able to use the nice native python if-then-else or match syntax.

rtpgOP1y 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#co...

philzook1y ago

Very interesting.

j / k navigate · click thread line to collapse