ATS

ATS est un langage de programmation conçu pour unifier la programmation avec des spécifications formelles. ATS prend en charge la combinaison de la démonstration du théorème avec la programmation pratique grâce à l'utilisation de systèmes de type avancés. Une version antérieure de The Computer Language Benchmarks Game a démontré que les performances d'ATS sont comparables à celles des langages de programmation C et C++. En utilisant la preuve de théorème et la vérification de type stricte, le compilateur peut détecter et prouver que ses fonctions implémentées ne sont pas sensibles aux bogues tels que la division par zéro, les fuites de mémoire, le dépassement de mémoire tampon et d'autres formes de corruption de mémoire en vérifiant l'arithmétique du pointeur et le comptage de références avant que le programme se compile. De plus, en utilisant le système de démonstration de théorème intégré de l'ATS, le programmeur peut utiliser des constructions statiques qui sont entrelacées avec le code opérationnel pour prouver qu'une fonction atteint sa spécification.

Texte : extrait de l'article Wikipédia « ATS (langage de programmation) », sous licence CC BY-SA 4.0.