complets, concurrent, temps réel en même temps que leur preuve sans que le coût à payer soit trop lourd ?
C'est exactement ce que les gens essaient de fournir quand ils écrivent des bibliothèques pour écrire du code concurrent/temps-réel : des fonctions à la sémantique bien définie, qui permettent de raisonner sur des morceaux de programmes en faisant abstraction des détails pénibles et répétitifs.
Après, l'idée n'est peut être pas de fournir des bases pour des preuves, mais on peut imaginer que cela puisse devenir un objectif.
Il y a d'autre part de la recherche en preuve pour les modèles distribués en utilisant des sémantiques de jeu, bien que cela soit au delà de mes compétences.
Enfin, si le langage lui-même est turing-complet, rien ne force toutes les parties du programme à être aussi expressives. Par exemple, on peut imaginer ajouter un DSL pour la concurrence, qui ne fait que ça et qui serait plus facilement analysable. Le tout est de bien gérer les interactions entre les différentes parties du programme.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par Aluminium95 . En réponse à la dépêche OCaml 4.03. Évalué à 3.
C'est exactement ce que les gens essaient de fournir quand ils écrivent des bibliothèques pour écrire du code concurrent/temps-réel : des fonctions à la sémantique bien définie, qui permettent de raisonner sur des morceaux de programmes en faisant abstraction des détails pénibles et répétitifs.
Après, l'idée n'est peut être pas de fournir des bases pour des preuves, mais on peut imaginer que cela puisse devenir un objectif.
Il y a d'autre part de la recherche en preuve pour les modèles distribués en utilisant des sémantiques de jeu, bien que cela soit au delà de mes compétences.
Enfin, si le langage lui-même est turing-complet, rien ne force toutes les parties du programme à être aussi expressives. Par exemple, on peut imaginer ajouter un DSL pour la concurrence, qui ne fait que ça et qui serait plus facilement analysable. Le tout est de bien gérer les interactions entre les différentes parties du programme.