It also overloads other methods to provide kind of symbolic objects.
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?
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!
Abstract interpretation is super easy to implement over Lisp-like languages IMO.
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
