Program synthesis

Stream: new members

[Uijel]

Has anyone ever thought of using Lean for program synthesis? Tactics synthesize proofs, I would like to synthesize algorithms

[Mark Fischer]

Are you thinking of something like logic programming where you define the constraints and the system attempts to solve them for you? Prolog-style something?

[Uijel]

Yes