ATS est un langage de programmation au système de typage extrêmement expressif qui supporte les types dépendants et les types linéaires. Il permet de faire de la programmation fonctionnelle ainsi que de la programmation impérative vérifiée, c’est à dire que par exemple l’arithmétique de pointeur ou la gestion explicite de la mémoire sont autorisés mais le compilateur vérifie statiquement qu’aucune erreur (par exemple de segmentation) ne pourra se produire à l’exécution. En plus de vérifier que les accès mémoire ne conduiront pas à des erreurs de segmentation, ATS permet également de faire de la programmation prouvée à plus grande échelle, en permettant d’écrire des propositions et des preuves arbitrairement complexes, et en permettant de faire vérifier statiquement au compilateur les algorithmes relativement à une certaine propriété qu’ils sont censés vérifier.
Toutes ces propriétés (et bien d’autres, ATS est un langage extrêmement riche), en font un langage très efficace, en plus d’être bien plus sûr que beaucoup d’autres langages.