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