Program synthesis is the systematic, usually automatic, construction of correct and efficient executable code from declarative specifications. We have developed this technology primarily for application in the domains of data analysis and state estimation. We were also interested in correctness issues, specifically regarding the formal certification of synthesized code.