Здравствуйте, VladD2, Вы писали:

DM>>Введение в ATS и зависимые типы

VD>Не хочешь объединить это все в полноценную статью и опубликовать на РСДН?

Можно. А в каком объеме и жанре? Сейчас там у меня несколько постов, в них описание не систематическое и неполное, на базе конкретных примеров. Последнее в серии — один очень большой пример с доказательством сортировки smoothsort. Рассказ про smoothsort получился шибко длинным и сложным, его почти никто не осилит, не думаю, что его следует включать. Если же пытаться сделать более полное и систематичное описание языка, это может вылиться в нехилый трактат. К тому же, ряд нетривиальных но интересных фич я еще сам не освоил. Самое простое сейчас — объединить, слегка причесав, три первых поста: введение с примером про фильтрацию IP-адресов, про доказательства и про ограничения арифметики в типах.