I think what you're referring to is code generation or extraction https://coq.inria.fr/doc/V8.11.1/refman/addendum/extraction.html https://coq.inria.fr/doc/V8.1

I think what you're referring to is code generation or extraction https://coq.inria.fr/doc/V8.11.1/refman/addendum/extraction.html 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/ 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.