(socallinuxexpo.org)
•
Leslie Lamport는 LaTeX의 초기 개발자이며 분산 시스템 분야의 선구자. 2013년 튜링상 수상
•
그가 SCaLE 22x 키노트에서 추상화의 중요성을 강조하며, 대부분의 프로그래머가 코딩과 언어에 몰두하지만, 코딩 전 추상적 사고와 설계가 핵심임을 지적함
발표 요약
•
여러분은 내가 동시성(Concurrency)에 대해 얘기하는 걸 기대할 수 있으나, 이에 대해 새롭게 말할 것이 없음
•
그러나 "Concurrent한 프로그램 작성"에 대한 통찰이 일반적인 모든 프로그래밍에도 적용됨
•
이 발표는 프로그래밍 전반에 관한 이야기임
알고리듬 vs. 프로그램
•
알고리듬: 언어와 무관한 추상적 아이디어. 프로그램보다 더 추상적이고 상위 수준의 개념
•
프로그램: 알고리듬을 특정 언어로 구현한 구체적인 형태. 프로그래밍 언어는 알고리듬을 표현하기에 너무 복잡함
•
알고리듬은 실행되지 않으며, 일반적으로 짧고 간단함
•
특히 동시성 관련 코드에서는 먼저 정확한 알고리듬을 정의하고 구현해야 함
배열 최대값 예제로 보는 추상화
•
단순한 문제라도 "무엇을 할 것인가(What)"를 명확히 정의해야 함
•
예: "정수 배열의 최대값 반환" → "모든 원소 이상인 최소 수 반환"
•
비어 있는 배열 처리도 사전에 정의 필요 (예: ∞ 사용)
•
이렇게 명확한 정의를 통해 더 간단하고 견고한 알고리듬(How) 을 도출 가능
•
프로그램 실행은 단순한 명령 순서가 아닌, 상태(state)의 연속
•
각 상태 전이는 코드의 한 부분 실행을 의미함
•
이러한 시각은 알고리듬의 올바름을 증명할 때 중요함 (불변식 사용 등)
복잡한 시스템을 위한 도구: TLA+
•
추상화를 정밀하게 표현하기 위해 정확한 언어가 필요
•
TLA+는 그런 용도로 설계된 도구
•
Amazon Web Services는 TLA+로 심각한 설계 결함을 사전에 발견
•
Rosetta 우주선의 OS인 Virtuoso도 TLA+ 기반으로 설계, 코드가 간결하고 안정적이었음
불완전한 사양에서도 추상화의 역할
•
예: 프리티 프린터는 정렬 기준이 주관적일 수 있음
•
그럼에도 불구하고 추상화된 규칙 세트를 정해두는 것이 디버깅과 유지보수에 중요
글쓰기와 사고의 관계
•
생각을 글로 적는 것이 사고를 명확하게 해줌
•
추상화는 단순히 머리로만 하는 게 아니라 글로 표현해야 효과적
•
Lamport는 자신의 수학적 훈련이 추상화 능력을 길러줬다고 언급
•
수학자들이 프로그래머에게 추상화를 가르칠 수 있음
라이브러리와 버그에 대한 시각
•
발표 2부 "왜 프로그램은 버그를 가져야 하는가"에서 복잡성 문제를 다룸
•
현대 소프트웨어는 많은 라이브러리에 의존하지만, 이들은 정확한 언어 독립적 설명이 부족
•
이로 인해 통합 과정에서 예상치 못한 버그가 발생
•
예: 본인의 TLA+ 강좌 사이트에서 JavaScript 디버깅 경험
•
상태 기반 시각이 이러한 복잡성을 이해하는 데 유용
질의응답에서 다룬 주제들
•
AI가 추상화에 미칠 영향
•
오픈소스와 학계의 단절
•
개발자들이 형식 정의(formal definition)를 소홀히 하는 현실
•
여전히 가장 중요한 것은 "코딩 전에 생각하기"
결론: 프로그래밍의 본질은 사고
•
Lamport는 단순한 코딩보다 추상적 사고와 형식적 사양을 우선시해야 한다고 주장
•
upfront 노력이 크지만, 결과적으로 더 견고하고 유지보수하기 쉬운 소프트웨어로 이어짐
•
코딩은 프로그래밍의 일부일 뿐, 진짜 프로그래밍은 정확한 알고리듬과 추상화에서 시작
•
시스템 복잡성과 동시성이 증가하는 현대에서 추상화는 필수 역량 이며, 사고하고 추상화하는 훈련이 프로그래머에게 필요함