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.
[0] https://www.csail.mit.edu/research/synquid-synthesis-liquid-...
[1] https://www.daxx.com/blog/development-trends/number-software...