Program synthesis, defined as the ultimate ideal of automatically generating correct, verifiable code directly from its specification, has been a central, yet persistently challenging, grand research problem for the programming languages community for decades. Researchers have tirelessly developed sophisticated techniques rooted in formal methods, semantic reasoning, and exhaustive search algorithms to achieve this goal, often focusing on correctness guarantees over scalability. However, the recent, dramatic wave of Large Language Models (LLMs) has not just incrementally improved the field; it has fundamentally remodeled the landscape, providing a new and powerful, albeit opaque, engine for code generation at unprecedented scale and fluency.

The core goal of this tutorial is to critically explore this transformative synthesis paradigm. While LLMs offer incredible fluency and speed, they often lack the necessary correctness and formal guarantees that decades of PL research have prioritized. We will discuss how to bridge this divide, arguing that foundational principles (including program semantics, type theory, and static analysis techniques) are in fact more crucial than ever for advancing LLM-powered synthesis into a reliable and trustworthy technology.

My research is in computer science, at the intersection of formal methods and machine learning. My interests include program synthesis, games, and automata. I am a senior researcher at CNRS in LaBRI, Bordeaux (research director) since 2025. The academic year 2022 - 2023 I was visiting University of Warsaw. Until recently I was a research fellow of The Alan Turing Institute of data science and artificial intelligence in London. I defended my PhD in October 2015 and my habilitation (HDR) in February 2022. I am the head of the Synthesis team in LaBRI since 2024.