Je viens d'assister à un excellent exposé de Viktor Kuncak sur la synthèse de programmes à partir de spécifications. Enthousiasmant ; on sent une recherche ambitieuse et vivante.

(Évidemment, mon enthousiasme est sans doute lié au fait que je proposais une approche très proche pour la synthèse de fonctions de transfert en interprétation abstraite, par élimination de quantificateurs. Ce que fait Viktor peut se voir comme une élimination constructive de quantificateurs.)