한줄평
“엄밀한 형식 증명이나 검증된 코드를 다루려는 연구자·개발자에게 적합합니다. 개념이 깊고 진입 장벽이 높아 가볍게 접근하기는 어렵습니다.”
이런 분께 형식 증명이나 검증된 소프트웨어를 다루려는 연구자·개발자께
좋은 점
- 증명을 기계적으로 검증해 오류를 차단
- 활발한 형식 수학 커뮤니티
아쉬운 점
- 학습 곡선이 매우 가파름
린 소개
수학적 증명을 컴퓨터로 검증할 수 있는 정리 증명기이자 프로그래밍 언어입니다. 정의와 정리를 코드로 적으면 논리적으로 빈틈이 없는지 기계가 확인해 줍니다. 형식 수학을 연구하거나 검증된 소프트웨어를 만들려는 사람에게 맞습니다. 컴파일러·대화식 도구를 제공하며 주로 편집기와 명령줄에서 씁니다.
