Как я стал соавтором статьи с Лесли Лэмпортом, которую сам же и отклонил
I came to write THAT paper with Leslie Lamport
Лоуренс Полсон рассказывает, как его рецензия на статью Лесли Лэмпорта «Types Considered Harmful» привела к неожиданному соавторству. Несмотря на первоначальное отклонение, редактор TOPLAS предложил Полсону и Лэмпорту переработать статью. Полсон описывает процесс совместной работы, второй раунд рецензирования и анализирует, насколько тезисы Лэмпорта о вреде типов выдержали проверку временем, признавая, что типизированные формализмы доказали свою ценность.
Без типов у вас нет перегрузки обозначений, что тривиально в принципе (можно просто использовать много разных символов), но очень важно на практике.
- joomy
Каким-то образом финальная версия статьи не прилинкована в посте: https://www.microsoft.com/en-us/research/publication/specifi...
- srean
> Второй рецензент, Дэвид МакАллестер, пришёл к тому же выводу.
Тот самый Дэвид МакАллестер, который ввёл PAC-байесовские границы?
Ответ: да.
- mrkeen
> В этой диссертации был смысл. Системы типов находились в состоянии flux в 1992 году, когда была написана эта заметка. Coq (теперь Rocq) только что появился, и в теории типов Мартина-Лёфа происходили большие изменения. Что касается простых теорий типов, ранние реализации HOL существовали всего пару лет. Было неясно, на что способно любое типизированное исчисление. Помощники доказательств ещё не поддерживали классы типов. Джон Харрисон был за годы до того, как ввёл свой трюк для получения дешёвых зависимых типов, который достаточно хорошо работает для выражения Tn.
Я не хочу вставлять линейные или зависимые типы в TLA+. Доказательство динамических свойств с помощью исчерпывающего рантайма — это совершенно другая игра, нежели то, что можно делать статически.
Но я хочу исключить бессмыслицу. Конечно, я могу доказать, что светофор никогда не равен RED_LIGHT. Плохо, если он равен RED.