Là ou c'est intéressant c'est quand on fait de la preuve de programme, ça élimine carrément (presque) certaines classes de failles, ce que Rust fait en partie.
La preuve formelle de programme c'est traditionnellement un gros effort et c'est très peu fait. Là quelqu'un de compétent peut faire ce qui aurait pris énormément de temps pour un programme non trivial, un compilateur, et prouver formellement une partie significative, en étant aussi assistant de l'IA que l'inverse. C'est assez remarquable et ça va bien plus loin que la chasse aux failles.
[^] # Re: Faut t'habituer
Posté par thoasm . En réponse au journal Les LLM: Langueur, Lassitude et Morosité. Évalué à 1.
Là ou c'est intéressant c'est quand on fait de la preuve de programme, ça élimine carrément (presque) certaines classes de failles, ce que Rust fait en partie.
C'est peut être passé un peu inaperçu mais, voir ce lien ... https://linuxfr.org/users/thoasm/liens/creation-supervisee-d-un-compilateur-prouve-formellement-par-de-l-iagen
La preuve formelle de programme c'est traditionnellement un gros effort et c'est très peu fait. Là quelqu'un de compétent peut faire ce qui aurait pris énormément de temps pour un programme non trivial, un compilateur, et prouver formellement une partie significative, en étant aussi assistant de l'IA que l'inverse. C'est assez remarquable et ça va bien plus loin que la chasse aux failles.