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

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