Jane Street adopte les méthodes formelles grâce à l'IA
Original : Formal methods and the future of programming
Pourquoi c'est important
Evolution majeure dans l'adoption des méthodes formelles grâce à l'IA
Jane Street change de position sur les méthodes formelles après 25 ans de scepticisme. L'émergence du codage par agents IA modifie l'équation coût-bénéfice, poussant l'entreprise à constituer une équipe dédiée.
Yaron Minsky de Jane Street explique le revirement de l'entreprise concernant les méthodes formelles. Historiquement coûteuses (seL4 a nécessité 25 années-personnes pour vérifier 8700 lignes de C avec 23 lignes de preuve par ligne), ces méthodes deviennent attractives avec l'IA générative. Les agents de codage réduisent les coûts d'utilisation tout en augmentant les bénéfices potentiels. Le code généré par IA tend vers la « médiocrité » avec des bugs et violations d'invariants, créant un goulot d'étranglement de vérification. Les méthodes formelles pourraient automatiser cette vérification et fournir le feedback nécessaire aux agents IA pour s'améliorer.