I was also looking into it to turn normal python functions into some kind of constraints. But as you point out in your article it cannot really work through python imperative statements like conditions and loops, so you either need to find a way to cover all code paths, or only use a subset of Python (like Z3 does to some degree I believe). I still need to try it out further.
For your proof assistant it seems you could indeed use it if you limit yourself to Python expressions. Interesting stuff!
Comments
This is exactly what the CrossHair library does: https://github.com/pschanely/CrossHair
It also overloads other methods to provide kind of symbolic objects.
This looks great! The paper linked in your README https://hoheinzollern.files.wordpress.com/2008/04/seer1.pdf also seems like a nice explanation of similar ideas.
The reason I'm exploring this idea is to use more natural looking python as dsl for function definitions in my proof assistant https://github.com/philzook58/knuckledragger
Also to see if I can make a nice-looking staged metaprogramming framework in python like buildit, but maybe to generate C/C++ rather than more python.
Could Crosshair be used in these ways?
To be clear I did not make CrossHair.
I was also looking into it to turn normal python functions into some kind of constraints. But as you point out in your article it cannot really work through python imperative statements like conditions and loops, so you either need to find a way to cover all code paths, or only use a subset of Python (like Z3 does to some degree I believe). I still need to try it out further.
For your proof assistant it seems you could indeed use it if you limit yourself to Python expressions. Interesting stuff!