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

C>Так вроде примеры неплохо гуглятся Idris-подобные языки позволяют описывать зависимые типы (завтипы по-русски) и проверять их целостность на этапе компиляции. Завтипы это типы данных, зависящие от данных Например, не просто "строка", а "строка-палиндром".

А не получится ли так, что мы вместо одной программы будем писать две, сравнимого размера? Одна будет в рантайме чего-то делать, другая будет во время компиляции проверять, что первая деляет всё правильно.