Le principe de ces trucs là, c'est de ne prouver "à la main" que vraiment les briques de bases, genre les fonctions vraiment de base.
De faire relire ces preuves super simple par pleins de gens, histoire d'être sûrs que ces preuves de bases sont correctes, et de construire l'implémentation en construisant toutes les bibliothèques à partir de ces briques de bases prouvées à la main, et en faisant tout vérifier par le prouveur de manière semi-automatique.
Alors certe, c'est un peu chateau de carte, mais c'est bien plus simple d'implémenter et de prouver et tester des briques de bases genre l'insertion d'un élément dans un tableau sans dépassement de capacité que de tester la JVM.
[^] # Re: [X] : C'est exactement ce que j'espérais
Posté par thoasm . En réponse au journal Sondage Java sous GPL, donnez votre avis à Sun. Évalué à 2.
De faire relire ces preuves super simple par pleins de gens, histoire d'être sûrs que ces preuves de bases sont correctes, et de construire l'implémentation en construisant toutes les bibliothèques à partir de ces briques de bases prouvées à la main, et en faisant tout vérifier par le prouveur de manière semi-automatique.
Alors certe, c'est un peu chateau de carte, mais c'est bien plus simple d'implémenter et de prouver et tester des briques de bases genre l'insertion d'un élément dans un tableau sans dépassement de capacité que de tester la JVM.