Как вы формально проверяете, что нет никаких арифметических или других исключений?

Это точно не грубая сила!

Было опробовано множество различных методов для установления арифметической безопасности с разной степенью успеха. Большая часть компьютерной арифметики в наши дни полностью формализована как в формализмах, таких как Isabelle/HOL, Coq, ACL2, так и во многих других средствах доказательства теорем; а также в более автоматизированных методах, таких как решение SMT. В этих системах вы получаете модель своей системы (либо написанную вручную, либо автоматически извлекаемую из фактического исходного кода), а затем вы доказываете, что в вашем исполнении нет путей, которые сталкиваются с переполнением/недостатком потока. Конечно, это легче сказать, чем сделать; но поддержка инструментов со временем неуклонно улучшалась.

Отличный документ, на который можно посмотреть, как можно более или менее автоматически обнаруживать арифметическое переполнение/опустошение, — это работа Николая в области SMT: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf Содержащиеся здесь ссылки также могут стать отличной отправной точкой для изучения других исследований в этом направлении.