I think this is the correct way to think about automated coding. The natural question is: why are we using a statistical model to control this search, and not a symbolic model?

Modern SAT and SMT solvers are excellent at searching spaces. There has already been work on biasing them with machine learning. Symbolic models for control, statistical models for bias. We should be thinking about how to apply this idea to practical, industrial software engineering tasks. There is already some work on program synthesis from formal specifications, but it has yet to scale.