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

R>Если выразить инварианты программы на уровне типов,

Выражай их и в C++ — самая развитая система типов среди mainstream языков

R>то успешность компиляции будет гарантировать успешность работы.

Все инварианты, пред/пост-условия в типах не выразишь.

R>но по крайней мере могу быть достаточно уверен, что ошибка не вызвана buffer overrun в какой-нибудь отдалённой части программы или кривой библиотеке.

В кривой библиотеке не может быть unsafe?