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