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

DG>т.е. насколько я понимаю, работа по исследованию — что надо задать, чтобы остальное можно было вывести автоматически — в ATS не проводится?

Затрудняюсь ответить. В определенных рамках автоматический вывод там есть: решатель арифметических соотношений довольно умен, а доказательства теорем часто выглядят как серия намеков — большую часть текста не приходится выписывать, ее компилятор сам выводит. Но менять за спиной у программиста определения типов и функций, добавлять параметры и вычисления компилятор не считает себя вправе, это момент идеологический. Вплоть до того, что есть явное различие между голой функцией (как в Си), замыканием с данными в управляемой куче и замыканием с данными, освобождаемыми вручную.