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


Что такое САР?

ATS – это язык программирования со статической типизацией, который объединяет реализацию с формальной спецификацией. Он оснащен очень выразительной системой шрифтов, основанной на структуре Applied Type System , которая дает языку его имя. В частности, в ATS доступны как зависимые типы, так и линейные типы.

Текущая реализация ATS2 (ATS / Postiats) написана на ATS1 (ATS / Anairiats) и состоит из более чем 180 K строк кода. ATS может быть столь же эффективным, как C / C ++, как по времени, так и по памяти, и поддерживает множество парадигм программирования, в том числе:

  • Функциональное программирование . Ядром ATS является функциональный язык вызова по значению, вдохновленный машинным обучением. Наличие линейных типов в ATS часто заставляет функциональные программы, написанные на нем, работать не только с удивительно высокой эффективностью (по сравнению с C), но и с удивительно малым объемом памяти (по сравнению с C).
  • Императивное программирование . Новый подход к императивному программированию в ATS прочно укоренился в парадигме программирования с доказательством теорем . Система типов ATS позволяет безопасно поддерживать в ATS многие функции, которые считаются опасными в других языках (например, арифметика с явным указателем и явное выделение / освобождение памяти), что делает ATS хорошо подходящим для реализации высококачественных низкоуровневых систем.
  • Параллельное программирование . ATS может поддерживать многопоточное программирование за счет безопасного использования потоков pthread. Доступность линейных типов для отслеживания и безопасного управления ресурсами обеспечивает эффективный подход к созданию надежных программ, которые могут использовать большие преимущества многоядерных архитектур.
  • Модульное программирование . Модульная система ATS в значительной степени основана на модуле Modula-3, который одновременно прост и универсален, а также эффективен для поддержки крупномасштабного программирования.

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


Для чего нужен САР?

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

Предложение по изучению ATS

ATS многофункциональна (как C ++). Предварительные знания функционального программирования на основе ML и императивного программирования на основе C могут быть большим плюсом для изучения ATS. В общем, следует ожидать встретить много незнакомых концепций программирования и функций в ATS и быть готовым потратить значительное количество времени на их изучение. Надеюсь, что в конце концов вы станете очень уверенным в себе программистом, который сможет получать удовольствие от реализации больших и сложных систем с минимальной потребностью в отладке.


Благодарности

Разработка ATS частично финансировалась Национальный научный фонд (NSF) в рамках грантов No. CCR – 0081316 / CCR – 0224244, нет. CCR – 0092703 / 0229480, нет. CNS – 0202067, нет. CCF – 0702665 и без CCF – 1018601. Как всегда, любые мнения, выводы, выводы или рекомендации, выраженные здесь, принадлежат авторам и не обязательно отражают точку зрения NSF.