ATS (язык программирования)

ATS (Applied Type System) — язык программирования, чьим основным предназначением являлась обеспечение поддержки доказательства теорем в сочетании с практическим программированием при использовании продвинутой системы типов данных. Производительность ATS сравнима с производительностями таких языков как Си и C++.

История

Большая часть ATS была позаимствована у языков программирования ML и Objective Caml. Предшествующий язык Dependent ML того же автора по сути включён в новый.

Проверка теорем

Основной целью ATS являлась поддержка проверки теорем в сочетании с практическим программированием.

Представление данных

Согласно автору (Хонвей Хи), эффективность ATS в основном зависит от способа представления данных в языке и оптимизации хвостовых вызовов (которые в целом весьма важны для эффективности функциональных языков программирования). Данные хранятся в простом (плоском) виде или преимущественно без вложенных представлений.

Дополнительные источники

• Домашняя страница ATS

Ссылки

• ATS benchmarks | Computer Language Benchmarks Game
• Discussion about the language’s efficiency (Language Shootout: ATS is the new top gunslinger. Beats C++.)
• Combining Programming with Theorem Proving