Dans un assistant de preuve qui permet aussi de programmer, le fait de pouvoir faire ça est une propriété "émergente" du système, c'est un style de preuve parmi d'autres (preuves par raffinement, par logique de programme, etc.). Par exemple, cette technique est utilisée dans le framework / la bibliothèque Bedrock, conçue pour écrire des programmes bas-niveau vérifiés dans l'assistant de preuve Coq.
[^] # Re: Perl6
Posté par gasche . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 2.
Dans un assistant de preuve qui permet aussi de programmer, le fait de pouvoir faire ça est une propriété "émergente" du système, c'est un style de preuve parmi d'autres (preuves par raffinement, par logique de programme, etc.). Par exemple, cette technique est utilisée dans le framework / la bibliothèque Bedrock, conçue pour écrire des programmes bas-niveau vérifiés dans l'assistant de preuve Coq.