프로그램 검증에서 Rocq가 Lean보다 나은 이유

- 수학 형식화에서 Lean의 성장세는 뚜렷하지만, 실행 가능한 프로그램 검증에는 네이티브 공귀납과 다양한 추출 경로, 축적된 검증 생태계를 갖춘 Rocq가 더 잘 맞음 - Rocq는 CoInductive 와CoFixpoint 로 공데이터를 선언하고 guardedness를 검사한 뒤 지연 실행 코드로 추출하지만, Lean에서는 라이브러리 인코딩·이터레이터·...