There are good reasons to need program synthesis in our industry.
There are domains in programming where the cost of errors is too high. Being able to specify requirements in a high-level language and synthesize the program from the specification would prove that there are no errors in the resulting program, assuming you trust the kernel, and bring the resulting cost of producing code that is free of those kinds of errors way down.
An example would be programming authorization control systems. Some enterprises require a stunning level of complexity that testing all the different combinations of authorization rules would be infeasible. Instead, if we can specify the rules in a rich type system, we can synthesize the program that implements the rules. Such a program would be, "correct by construction."
Take a look at projects like Synquid [0] -- it's a really cool idea.
There are 26-29M software developers in the world [1], which accounts for less than 0.9% of the global workforce. We can do with making programming more accessible.
