Leslie Lamport와 함께 '그 논문'을 쓰게 된 이야기
I came to write THAT paper with Leslie Lamport
1992년, Leslie Lamport는 'Types Considered Harmful'이라는 논문을 제출했지만, 저자 Lawrence C. Paulson을 포함한 심사자들은 이를 거절했습니다. 그러나 편집자 Andrew Appel의 제안으로 Paulson은 Lamport와 공동 저자가 되어 논문을 개선하게 됩니다. 이후 두 번째 심사에서도 거절당했지만, 결국 게재되었습니다. 이 글은 그 과정을 회고하며, 27년 후 타입 시스템이 어떻게 발전했는지, 그리고 Lamport의 주장이 얼마나 유효했는지 평가합니다.
타입이 없는 형식주의는 표기법의 오버로딩을 지원하지 않는데, 이는 원칙적으로는 사소하지만 실제로는 큰 문제입니다.
HN 토론
11- joomy
어쩐지 블로그 포스트에 논문 최종본 링크가 없네: https://www.microsoft.com/en-us/research/publication/specifi...
- srean
> 다른 심사위원인 David McAllester도 같은 결론에 도달했다.
PAC-Bayesian 경계를 도입한 그 David McAllester가 맞나?
답: 그렇다.
- mrkeen
> 이 논지에는 일리가 있었다. 1992년 그 메모가 작성되었을 당시 타입 시스템은 격변의 시기에 있었다. Coq(현재 Rocq)은 막 등장했고, Martin-Löf 타입 이론에는 큰 변화가 일어나고 있었다. 단순 타입 이론에 관해서는, HOL의 초기 구현이 등장한 지 불과 몇 년밖에 되지 않았다. 어떤 타입 계산법이 무엇을 할 수 있을지 불분명했다. 증명 보조 도구는 아직 타입 클래스를 지원하지 않았다. John Harrison이 저예산 의존 타입을 얻는 그의 트릭을 도입하기까지는 몇 년이 남아 있었는데, 그 트릭은 Tn을 표현하기에 충분히 잘 작동한다.
나는 TLA+에 선형 타입이나 의존 타입을 넣고 싶지 않다. 철저한 런타임으로 동적 속성을 증명하는 것은 정적으로 할 수 있는 것과는 완전히 다른 게임이다.
하지만 나는 무의미한 것을 배제하고 싶다. 물론, 신호등이 절대 RED_LIGHT와 같지 않다는 것을 증명할 수 있다. 만약 그것이 RED와 같다면 곤란하다.