수학자에게 Lean이 있다면 개발자에게는 TLA+가 있다

2 hours ago 1

프로그래밍은 거칠게 말하면, 내가 만든 논리가 틀리지 않았는지 사용자에게 배포해 런타임을 실행으로 증명하는일
- 배포 뒤 사용자가 발견하던 논리의 허점을, 배포 전에 더 많이 찾아낼 수는 없을까?

수학의 증명과 프로그래밍의 타입 검사는 생각보다 가까움
- 커리–하워드 대응에서는 명제를 타입으로, 증명을 그 타입의 프로그램으로 표현함
- 증명을 구성하고 검사하는 일이 프로그램을 작성하고 타입을 검사하는 일과 연결됨
수학자에게 증명을 검사하는 Lean이 있다면, 개발자에게는 동시성 설계를 명세하는 TLA+와 모델 검사기 TLC가 있음
- 내가 고른 테스트 케이스뿐 아니라, 설정한 유한 모델이 허용하는 실행을 탐색해 조건을 깨뜨리는 반례를 찾음
타입 검사도 통과하고 유닛 테스트도 성공했는데, A가 B보다 먼저 끝났다는 이유만으로 프로그램이 깨질 수 있음
- 각각 내부 순서를 지키는 10단계 작업 두 개의 실행을 섞는 방법만 184,756가지. 상태보다 어려운 것은 순서

RxJS에서 먼저 끝난 작업이 다른 작업의 공유 연결까지 닫아버리는 문제를 작은 TLA+ 명세로 옮기는 예시 포함
- “작업이 하나라도 실행 중이면 연결은 열려 있어야 한다”는 조건과 TLC 검사 설정·명령을 제시
테스트 주도 개발과 유닛 테스트에는 늘 작성·유지 비용이 따랐지만, AI는 테스트 초안을 만드는 비용을 크게 낮추고 있음
- 같은 방식으로 상태 모델과 검사 조건의 초안도 작성할 수 있음

이제 다음 ‘공짜 점심’ 후보는 동시성 검증
- 개발자를 괴롭히는 병렬·비동기 실행 순서를, 유닛 테스트를 추가하듯 작은 TLA+ 모델로 배포 전에 검토해보자는 제안

Read Entire Article