Вообще, спор "теоретиков" и "практиков" возникает очень много где. Но вы уверены, что этот "практик компиляторостроения" действительно стоял у истоков компилятора?

В сети где-то относительно недавно пробегала совершенно общая выжимка исследований на тему, как писать программы. Ну там, в общем банальности для людей здесь - что чем раньше мы выловим ошибку кодирования, тем меньше она будет стоить (стоимость растёт по экспоненте) и т.д.

В частности, проговаривался один факт - что для вылавливания ошибок архитектуры нужно как можно быстрее сделать костяк, работающий от и до. И уже потом наращивать его мясом. Чтобы не получилось ситуации, когда мы роем тоннель с двух сторон, а получаем два тоннеля.

То есть, фактически, надо проработать подзадачи с самым высоким риском.

Но если у нас нет взгляда на проект с высоты птичьего полёта (см статью Дайсона Birds and Frogs), мы не можем быстро убрать тупиковые ветви в архитектуре. И проект может умереть под собственным весом.

Когда что-то делают быстрее быстрее, то получается черт знает что в половине случаев.
Зависит от ситуации.
Наилучшим сигналом для начала написания кода служит полнота информации о предметной области. То что "иногда" она достигается сразу - всего лишь совпадение.

Проблема лишь в том, что определить полноту информации о предметной области можно как правило постфактум, а то и вовсе втянувшись в дело и наломав дров. (привет попаданцам в прошлое, которые знают "как надо")

Если же есть проблемы в архитектуре, которые не позволяют ей лишиться какого-нибудь большого куска кода и принять совершенно другой, то это вопросы к архитектору. А то на собеседованиях мозги всякими бандами и солидами парят, а на деле видишь, что эти люди не умеют конвеер по обработке огромной задачи в виде последовательности маленьких реализовать. А то и вовсе под архитектурой пониманиют квадратики с текстом внутри и стрелочкой "туда".

С одной стороны, в случае конкретно Котлина команда сразу говорила, что language reference они напишут (хотя бы не формальный, но полный), но уже после версии 1.0 и вообще когда будет больше времени или типа того.

Кажется, для этого язык нужно как минимум заморозить.

Ну как бы естественно. Можно конечно сделать формальную спецификацию для MVP, но все равно в процессе даже этого MVP будет множество изменений, дополнений и уточнений которые вынудят вносить изменения и в спецификацию, а это отнимает время и ресурсы, которые и так ограничены вначале пути у любой команды

Гипотеза в том, что если у тебя есть какой-то высокоуровневый способ формально специфицировать и верифицировать семантику языка, то ты сможешь экспериментировать с фичами бысрее (за счёт высокого уровня абстракции) и в перспективе сэкономишь немало времени на необходимости отлавливать и исправлять тонкие unsoundness баги.

unsoundness баги можно отловить и через fuzzing тестирование сейчас, при этом сами тесты пишуться всего один раз, в отличии от постоянных правок спеки. Хотя конечно, если есть инструмент которые умеет превращать спеку в реализацию каким то образом это бы упростило эксперименты, но на это нужно потратить много ресурсов, а по окончании все опять переписать «с нуля» для оптимизации, и в процессе этого все равно выплывут баги, все равно придется писать тесты и фаззинг)

> unsoundness баги можно отловить и через fuzzing тестирование

Я бы посмотрел на такой отлов багов с Rust Pin и багов в многопоточном коде. 😉

> при этом сами тесты пишуться всего один раз, в отличии от постоянных правок спеки

Это выглядит протеворечивым: как так оказывается необходимо менять спеку, но тесты менять не нужно?

> все опять переписать «с нуля» для оптимизации

Это да, есть такая проблемка. Люди с этим борются, но окончательного решения пока нет. 😞

Есть какой то ЯП новый не помню название, но там что бы его попробовать нужно установить Coq, Ocaml, Ruby и Java (или Python не помню уже) + либы. Ну его нафиг)

> Это выглядит протеворечивым: как так оказывается необходимо менять спеку, но тесты менять не нужно?

Чаще всего дополнять, но даже те измения будет вносить намного проще