Est-ce que l'algo seul peut être prouvé sans que le programme complet soit prouvé ? Je ne sais pas.
Alors, tout dépend de la techno utilisée.
De ma petite expérience en Spark, on peut prouver des morceaux du programme en ne marquant que certaines unités de compilation comme étant en Spark.
Typiquement, les entrées/sorties sont exclues du sous-ensemble vérifiable par Spark.
Mais, il faut bien voir qu'il faut quand même écrire les annotations Spark dans le code Ada pour pouvoir prouver quoique ce soit et ça, c'est pas forcément toujours très aisé.
Côté Rust il y a quelqu'un qui travaille dessus
Après, j'ai aussi vu un Coq2Rust permettant donc de créer son programme Rust à partir d'un programme Coq mais j'avoue ne pas avoir regardé plus que ça.
[^] # Re: Preuves ?
Posté par Blackknight (site web personnel, Mastodon) . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 3.
Alors, tout dépend de la techno utilisée.
De ma petite expérience en Spark, on peut prouver des morceaux du programme en ne marquant que certaines unités de compilation comme étant en Spark.
Typiquement, les entrées/sorties sont exclues du sous-ensemble vérifiable par Spark.
Mais, il faut bien voir qu'il faut quand même écrire les annotations Spark dans le code Ada pour pouvoir prouver quoique ce soit et ça, c'est pas forcément toujours très aisé.
Après, j'ai aussi vu un Coq2Rust permettant donc de créer son programme Rust à partir d'un programme Coq mais j'avoue ne pas avoir regardé plus que ça.