Типы для языка программирования не обязательны

Речь шла про верификацию

ну там конкретно написано

We advocate for a system focused on pushing workflow integration as early as possible. When possible, checks are enabled as compiler errors. To avoid breaking builds, tool writers take on the task of first fixing all the existing issues in the codebase, allowing us to "ratchet" the quality of Google's codebase one small step at a time, without regressions. Since we present the errors in the compiler, developers encounter them immediately after writing code, while they are still amenable to making changes.

типа лучше всего при компиляции, если не получается то при коммите

Так что было бы правильнее говорить не о тайпчекере для самого языка, так как типов в языке может не быть

Ассемблерный код вот тоже верифицировать можно

Ну, да. Но у Google есть разные компиляторы. Некоторые с Хоаровской логикой, а не с типами. Woofs, например. И народ, всё равно, умудряется косячить :)

хоаровскую логику тоже надо внедрять в типы, у меня научник считай всю карьеру на этом построил ;)

Ох уж эта идеология! Был бы способ механизации без типов, на практике можно было бы и без типов.

Надо, наверное. Я просто к тому, что это не спасает. Спецификации писать не легче, чем код.

ну вообще странное утверждение, так можно сказать что проектировать дома сложнее чем их строить, поэтому долой чертежи

Программа и есть чертёж.

Были такие дебаты: программист - это рабочий или инженер? Сошлись на втором :) Компилятор и язык - это кульман.

а если бы не существовало проблемы останова, так и вообще программисты не нужны были бы

Кажется ваше обсуждение для второго чата годится, а не для этого.

Так неразрешимость проблемы останова для класса автоматов — это математический факт

А то, что нельзя иначе механизировать, кроме как типами — не факт

Так какой вывод, бутстраппинг запрещаем? В каждом компиляторе С++ на С++ и компиляторе C# на C# сидит по брадобрею?

А компилятор Раста надо срочно на Го переписать, чтобы циркуляции такой не было.

выметем фикспоинты каленой метлой