Le but des deux langages est très différent, principalement du au fait qu'ATS n'est qu'a moitié un langage de programmation l'autre moitié étant une theorem prover (comme Coq).
On peut tracer un parallèle entre Rust/ATS et Haskell/Agda.
ATS dispose des types dépendants, ce qui veut dire que les types sont manipulables comme des valeurs et que les valeurs peuvent apparaitre dans les types. Ça semble simple dit comme ça, mais ça ne l'est pas du tout. Le typechecking devient très compliqué et demande souvent plus d'annotation, en contrepartie on peut vérifier statiquement bien plus de chose.
Un exemple : on peut encoder dans les types que les accès tableaux ne sont jamais out of bound. C'est génial ! Oui, mais ca veut dire que dès que tu fais un accès, tu dois prouver (via des manipulations sur les types, qui sont parfois devinée par le compilateur, mais pas toujours) que l'entier que tu utilises est bien dans les bornes. Ca c'est un exemple simple, mais on peut encoder des choses bien plus complexes.
Je ne sais pas trop comment ATS se comporte vis a vis de la terminaison, mais en Agda, tout programme doit terminer, il sait souvent le deviner tout seul .. mais pas toujours, et dans ce cas, il faut fournir la preuve.
La, on atteins un point ou il faut choisir : soit tu as de plus en plus de type safety, au prix d'annotations et de convolution parfois véritablement complexes, soit tu laisses passer des choses, mais ton compilateur sait inférer tout ce dont il a besoin.
Je me suis un peu étalé, mais je pense que ça répond a la question.
[^] # Re: Rust et ATS
Posté par Drup . En réponse à la dépêche Présentation de Rust 0.8. Évalué à 7.
Le but des deux langages est très différent, principalement du au fait qu'ATS n'est qu'a moitié un langage de programmation l'autre moitié étant une theorem prover (comme Coq).
On peut tracer un parallèle entre Rust/ATS et Haskell/Agda.
ATS dispose des types dépendants, ce qui veut dire que les types sont manipulables comme des valeurs et que les valeurs peuvent apparaitre dans les types. Ça semble simple dit comme ça, mais ça ne l'est pas du tout. Le typechecking devient très compliqué et demande souvent plus d'annotation, en contrepartie on peut vérifier statiquement bien plus de chose.
Un exemple : on peut encoder dans les types que les accès tableaux ne sont jamais out of bound. C'est génial ! Oui, mais ca veut dire que dès que tu fais un accès, tu dois prouver (via des manipulations sur les types, qui sont parfois devinée par le compilateur, mais pas toujours) que l'entier que tu utilises est bien dans les bornes. Ca c'est un exemple simple, mais on peut encoder des choses bien plus complexes.
Je ne sais pas trop comment ATS se comporte vis a vis de la terminaison, mais en Agda, tout programme doit terminer, il sait souvent le deviner tout seul .. mais pas toujours, et dans ce cas, il faut fournir la preuve.
La, on atteins un point ou il faut choisir : soit tu as de plus en plus de type safety, au prix d'annotations et de convolution parfois véritablement complexes, soit tu laisses passer des choses, mais ton compilateur sait inférer tout ce dont il a besoin.
Je me suis un peu étalé, mais je pense que ça répond a la question.