명세로부터 효율적인 프로그램을 도출하는 체계적 방법

형식적으로 검증된 단계별 변환을 통해 명세(specification)로부터 효율적인 프로그램(program)을 체계적으로 도출하는 것은 Richard Bird Lambert Meertens가 80년대에 제시한 아름다운 아이디어였습니다. AI 코딩 에이전트와 AI 정리 증명기(theorem prover)의 등장으로 마침내 그 시대가 왔다고 생각합니다. 저는 이것이 사람이 이해할 수 있는 설명(working out)과 함께, 생성된 코드 자체가 올바르도록 하는(correct by construction) AI 코딩 에이전트의 기반을 형성할 수 있다고 생각합니다. 첨부된 기사에서는 Richard Bird의 고전적인 예제 중 하나를 Lean 4로 재현하고, 증명 및 성능 결과도 보여줍니다.