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

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

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

Ага, ага. Вы это уже делаете — в виде тестов. Если они у вас конечно есть. И ещё ручного тестирования, если вы конечно его проводите.

А в случае известного мне вида доказуемого кода, тесты — это декларации о том, что должен делать код, а сверкой деклараций и самого кода занимается верификатор, SMT.