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

Понятно, что совсем не факт, что строгий приказ "всем использовать линтеры" будет хоть кто-то выполнять :) Поэтому я такой сторонник формальных подходов (TLA+, Dafny...), т.к. рекомендация сразу превращается в сделку "всё или ничего": либо ты полностью доказываешь отсутствие ошибок в коде, либо в прод не комитишь. Но это стоит существенно дороже в плане ресурсов, и для мэйнстрима вообще не актуально.

Но я специально разбираю эти темки в СИ и ФА, потому что, поймите! что вам не нужно доказывать правильность вашего кода (это когда вы пишете доказательства на языках с завтипами, теорем-пруверах, где они в разы больше исходного кода). Вы доказываете (возможно, только в своём уме) соответствие кода вашей спецификации (которая, возможно, тоже живёт только у вас в уме, и это норм; но она должна существовать там эксплицитно, как явное знание), и это уже чисто про семантику и про мета-спеки, это "думательная машинка", которую крайне важно себе встроить. И в работе с нейронками будет в разы проще и легче.