Dans un vieux journal, je parlais d'un langage que j'ai tenté décrire suivant la mode des langages systèmes, un truc qui ressemble a du xml mais avec une notion de nommage pour faire des graphs acycliques. Le truc est mal définit mais bon. Je me demandais si il n'était pas plus sage d'utiliser un truc costaux comme coq ou pourquoi pas why3 pour vérifier le fichier au lieu de le faire à la main. L'idée est d'avoir un langage structurel très user-friendly, dont la vérification est sous traité. L'idée est qu'un langage structurel est plus facile à vérifier.
[^] # 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é à 3.
Dans un vieux journal, je parlais d'un langage que j'ai tenté décrire suivant la mode des langages systèmes, un truc qui ressemble a du xml mais avec une notion de nommage pour faire des graphs acycliques. Le truc est mal définit mais bon. Je me demandais si il n'était pas plus sage d'utiliser un truc costaux comme coq ou pourquoi pas why3 pour vérifier le fichier au lieu de le faire à la main. L'idée est d'avoir un langage structurel très user-friendly, dont la vérification est sous traité. L'idée est qu'un langage structurel est plus facile à vérifier.
"La première sécurité est la liberté"