A new software engineering paradigm – Blog

Dans ce billet, j'aimerais rassembler quelques réflexions sur ce que je crois être un nouveau paradigme en ingénierie logicielle. Il est réalisable aujourd'hui, et mes collègues et moi l'avons utilisé avec succès ces deux dernières semaines. En bref, le paradigme combine vérification formelle et IA :

• Les humains spécifient ce qu'ils veulent que le logiciel fasse dans un langage formel comme Lean.
• L'IA écrit le logiciel et une preuve formelle qu'il respecte la spécification. La preuve est vérifiable par machine, éliminant le besoin de relecture humaine de l'implémentation générée.

L'IA seule souffre du goulot de la relecture

Je crois que cette combinaison de vérification formelle et d'IA est bien plus efficace que l'IA seule. La raison : la revue de code. Même si les agents peuvent écrire du code à coût marginal quasi nul, relire tout ce code devient le nouveau goulot d'étranglement.

Alors pourquoi ne pas « YOLO » et abandonner la revue ? Dans certains domaines, ce serait peut-être acceptable. Mais pour la plupart des codebases, l'IA devrait d'abord devenir beaucoup meilleure. Ma façon de le voir : l'IA est peut-être aujourd'hui à peu près au niveau d'un seul humain pour écrire du code. Un développeur seul peut maintenir la qualité, mais ne peut pas passer à l'échelle ; les équipes humaines scalent en distribuant le travail et en utilisant la revue de code pour maintenir la qualité. L'IA scale l'écriture sans scaler la relecture, créant un goulot.

Notez que je ne parle pas d'avions ici. Beaucoup de logiciels « ordinaires » ne sont pas assez critiques pour justifier une vérification formelle en soi, mais ils le sont assez pour qu'on ne veuille pas non plus les livrer à l'aveugle. Le point clé de ce billet : la vérification formelle est un moyen d'utiliser l'IA plus efficacement. La hausse d'assurance est presque un effet secondaire.

Éliminer le goulot de la relecture

L'approche vérification formelle + IA peut éliminer la relecture humaine du code d'implémentation généré de deux manières. D'abord, en supposant que la spécification capture le comportement voulu, on n'a plus à se soucier de la correction du code. Ensuite, si le code est entièrement géré par l'IA, sa maintenabilité et sa lisibilité humaine deviennent moins importantes.

Le cadre général est le suivant :

• Les humains définissent les contraintes dures : ce sont les propriétés requises du logiciel, exprimées comme une spécification formelle. Elles capturent généralement une notion de correction.
• Les humains définissent les objectifs d'optimisation : les benchmarks mesurent ce que le code doit optimiser. Exemples évidents : le temps d'exécution et l'usage des ressources, mais les objectifs peuvent aussi inclure des propriétés difficiles à formaliser, testables expérimentalement.
• Les agents écrivent le code et les preuves : chaque changement proposé s'accompagne d'une preuve formelle que le logiciel satisfait les contraintes dures. Les benchmarks [...].