A new software engineering paradigm – Blog
L'auteur défend un nouveau paradigme d'ingénierie logicielle combinant vérification formelle et IA, déjà expérimenté avec succès par son équipe. L'humain spécifie le comportement attendu dans un langage formel comme Lean ; l'IA écrit à la fois le code et une preuve machine-vérifiable qu'il respecte la spécification, ce qui supprime le besoin de relecture humaine de l'implémentation. Le point central : l'IA fait passer à l'échelle l'écriture de code mais pas sa relecture, créant un nouveau goulot d'étranglement. La vérification formelle est présentée comme un moyen d'utiliser l'IA plus efficacement, la hausse d'assurance n'étant presque qu'un effet secondaire.
Lire l'analyse complète →