#Lean

타입 검사도 통과, 테스트도 통과 — 그런데 왜 순서 때문에 깨질까? 개발자를 위한 TLA+ 입문

수학자에게 증명을 검사해 주는 Lean이 있다면, 개발자에게는 동시성 설계를 명세하고 검증하는 TLA+와 모델 검사기 TLC가 있습니다. 배포 후에야 사용자가 찾아내던 논리의 허점을, 배포 전에 기계의 힘으로 먼저 찾아보자는 이야기입니다.