Thanks for the detailed break-down and the links!! > which are pretty much always mathematically uninteresting), then...absolutely! SAT/SMT are at the core of

Thanks for the detailed break-down and the links!! > which are pretty much always mathematically uninteresting), then...absolutely! SAT/SMT are at the core of constraint-based synthesis. Wow this is super cool to know! > http://www.pathsensitive.com/2021/03/why-programmers-shouldnt-learn-theory.html http://www.pathsensitive.com/2021/03/why-programmers-shouldn... This would definitely help to kickstart my journey in program synthesis:) > "egg: Fast and Flexible Equality Saturation"... It uses code trees, which I read about a few months earlier in the Handbook of Automated Reasoning > http://cubix-framework.com/ http://cubix-framework.com/ > https://egraphs-good.github.io/ https://egraphs-good.github.io/ > https://people.csail.mit.edu/asolar/ https://people.csail.mit.edu/asolar/ > https://github.com/microsoft/prose https://github.com/microsoft/prose These stuff are super cool! Really appreaciate it!