Logic in Computer Science plays important roles ranging from formal methods to Human-Computer Interaction, including Software and Hardware Engineering, etc. Regarding the former broad application domain of formal methods, a tremendous amount of work concern verification, namely satisfiability checking (for model synthesis) and model checking (for counterexample/witness synthesis). I want to discuss a fairly novel question, called Formula Synthesis Problem, that I believe is extremely natural to address, and yet has not received enough attention in logic. In its most general form, the Formula Synthesis Problem consists in deciding whether some formula in a given set is satisfied by a given model (and output one if any). Obviously, if the input set of formulas is finite, this amounts to model checking. On the contrary, if this set is infinite, say obtained by some tree-grammar for formulas, then the answer becomes extraordinary challenging. As far as I am aware of, only in [17], the authors (part of which I am) have addressed the problem for the first time, in the particular case of the logic Propositional Dynamic Logic (PDL) extended with shuffle ( \(\textsc {PDL}^{\mid \mid }\) ), a deeply-studied logic in the literature. The obtained results regarding this instance of the Formula Synthesis Problem, called \(\textsc {synthPDL}^{\mid \mid }\) , were published in a strongly AI-tainted conference, since it is AAAI 2022. I wish hereby to let these results be known by a broader audience, and in particular by the community of logic and formal methods. This, all the more than the contribution on \(\textsc {synthPDL}^{\mid \mid }\) opens up connections to other problems in other Computer Science fields such as planning and security.