Plein de choses :
- ton exemple n'a rien à voir avec un truc réel. Je parlais de typage statique, le genre de truc que l'on trouve dans ocaml, qui ne permet pas ce que tu écris.
- ton exemple n'a jamais été passé dans un prouveur automatique, la démo est manuelle (frama-c ?)
- il faut que l'expressivité soit compréhensible par le commun des mortels, why3 a l'air sympa comme coq, mais il faut être un matheux pour s'en servir. frama-c est un sous ensemble du C, et n'est même pas optimisant !
- c'est très rare d'avoir une spécification aussi simple, un compilo qui optimise, on compare le comportement de sa génération de code sans optimisation, et on colle un fuzzer devant. Imagines le bordel de convertir 500 HLR dans ce genre de langage.
- pour avoir bosser avec un prouveur, l'idéal est de pouvoir écrire un truc dans le même langage et lui demander si la sortie est toujours vrai. Dans le cas contraire, il fournit un contre-exemple. C'est juste énorme. En général, il répond qu'il ne sait pas faire.
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Plein de choses :
- ton exemple n'a rien à voir avec un truc réel. Je parlais de typage statique, le genre de truc que l'on trouve dans ocaml, qui ne permet pas ce que tu écris.
- ton exemple n'a jamais été passé dans un prouveur automatique, la démo est manuelle (frama-c ?)
- il faut que l'expressivité soit compréhensible par le commun des mortels, why3 a l'air sympa comme coq, mais il faut être un matheux pour s'en servir. frama-c est un sous ensemble du C, et n'est même pas optimisant !
- c'est très rare d'avoir une spécification aussi simple, un compilo qui optimise, on compare le comportement de sa génération de code sans optimisation, et on colle un fuzzer devant. Imagines le bordel de convertir 500 HLR dans ce genre de langage.
- pour avoir bosser avec un prouveur, l'idéal est de pouvoir écrire un truc dans le même langage et lui demander si la sortie est toujours vrai. Dans le cas contraire, il fournit un contre-exemple. C'est juste énorme. En général, il répond qu'il ne sait pas faire.
"La première sécurité est la liberté"