Impressive work. I once implemented sybolic execution in Lua to automate calculating error propagation for physics class, but when I tried to extend the system, I couldn't figured out how to deal with control structures and resorted to writing functions like ifElse(x, y, z). Feels good to find out it is possible after all.
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!
Isn't this kind of thing exactly why Lisp was so popular for symbolic computation historically?
Here some expression builder, with few renderers thereof, in one file, with some tests (beware: from 2012-2016)
Was used to turn a python function into plain text (textualize itself), into SQL-text (applicable as query), evaluate-numerically, translate into other languages, and the like.
https://github.com/svilendobrev/svd_util/blob/master/expr.py
This looks like a nice reflection of python into a syntax tree, but unless I'm mistaken, it can't reflect python control structures like if-then-else? Z3 or sympy already are kind of ready to go systems that overload all the typical operators. Is there something you've done here they are missing?
This is only expressions - what you can put inside a lambda. if-then-else are statements. The ternary op (Y if X else Z) probably was not yet there in 2012 - or i did not needed it. But You can add all other dunder operators if u need them..
This is the kind of thing I love to come across on a holiday break that seems ripe for side projects... :)