Moi je ne trouve pas cela choquant, parce que c'est une validation formelle qui a été faite :
> The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.
C'est de la validation formelle, c'est à dire prouvée mathématiquement. Mais attention, ca ne prouve pas qu'il n'y a pas de bugs ou que le code est parfait, ca prouve simplement que le code du noyau répond aux spécifications formelles établies par ses concepteurs.
Vulgairement ca veut dire que les mecs sont sûrs que ce qu'ils ont codé répond exhaustivement (et uniquement) aux besoins. La validation formelle (et pas uniquement de code source) est un domaine certes pas nouveau mais pas encore très répandu. Surtout parce qu'il ne serait pas rentable dans tous les domaines. Vu le temps nécessaire à valider formellement un modèle, et le fait qu'il ne fasse "que" dire "OK, je retrouve toutes tes specs formelles dans ton modèle/ton code", c'est plus de l'utilité des mecs qui conçoivent des moteurs d'avion ou des satellites que pour le logiciel de retouche photo de ma maman...
Le code source de la vérification doit exister quelque part mais ne donnera pas plus de valeur à cette validation. La validation en elle-même est suffisante puisqu'elle mettra des liens entre le code source et les exigences des specs, point.
[^] # Re: Avis de Linus Torvalds sur les micro-noyaux
Posté par Babelouest (site web personnel) . En réponse à la dépêche Entretien avec Andrew Tanenbaum à propos de MINIX. Évalué à 3.
Moi je ne trouve pas cela choquant, parce que c'est une validation formelle qui a été faite :
> The C code of the seL4 microkernel correctly implements the behaviour described in its abstract specification and nothing more.
C'est de la validation formelle, c'est à dire prouvée mathématiquement. Mais attention, ca ne prouve pas qu'il n'y a pas de bugs ou que le code est parfait, ca prouve simplement que le code du noyau répond aux spécifications formelles établies par ses concepteurs.
Vulgairement ca veut dire que les mecs sont sûrs que ce qu'ils ont codé répond exhaustivement (et uniquement) aux besoins. La validation formelle (et pas uniquement de code source) est un domaine certes pas nouveau mais pas encore très répandu. Surtout parce qu'il ne serait pas rentable dans tous les domaines. Vu le temps nécessaire à valider formellement un modèle, et le fait qu'il ne fasse "que" dire "OK, je retrouve toutes tes specs formelles dans ton modèle/ton code", c'est plus de l'utilité des mecs qui conçoivent des moteurs d'avion ou des satellites que pour le logiciel de retouche photo de ma maman...
Le code source de la vérification doit exister quelque part mais ne donnera pas plus de valeur à cette validation. La validation en elle-même est suffisante puisqu'elle mettra des liens entre le code source et les exigences des specs, point.