That's usually called program synthesis, and a lot of it uses formal methods. It isn't usually considered AI (but recently the field started incorporating a lot of ML, like pretty much anything in CS these days.)

Correct me if I'm wrong, but I think program synthesis works more from writing very general formal specifications, rather than learning from a sample of desired outputs.

The latter is called Programming By Example, and the pattern-finding process needed to infer generalities from specific samples does benefit from machine learning techniques.

"programming by example" is a form of program synthesis, where the spec is provided by the examples. It is a formal specification, albeit incomplete. Program synthesis, as a concept, does not require the specification to be complete.