ATS: язык, в котором типы доказывают, что программа не упадёт
Introduction to Programming in ATS
Книга Hongwei Xi знакомит с ATS — языком, объединяющим функциональное программирование, зависимые и линейные типы, а также доказательство теорем. Читатель проходит путь от простых типов и алгебраических типов данных до программирования с доказательствами (PwTP), работы с представлениями (views) для управления памятью и шаблонов. Материал плотный и рассчитан на тех, у кого уже есть серьёзный опыт программирования.
Будучи языком программирования, ATS богат как синтаксисом, так и возможностями.
- srean
Раньше ATS довольно много обсуждали на HN
https://hn.algolia.com/?query=The%20ATS%20Programming%20Lang...
MLton и Felix — это ещё два языка, вдохновлённых ML, которые оптимизируют всю программу целиком, чтобы генерировать быстрый код.
- ddellacosta
Забавный доклад про этот язык вот здесь: https://www.youtube.com/watch?v=zt0OQb1DBko («A (Not So Gentle) Introduction To Systems Programming In ATS» от Aditya Siram)
- drop_star
Abstract Tree Syntax