Lean, 완벽해질 수 있는 프로그래밍 언어

Alok Singh은 개인 블로그를 통해 Lean을 '완벽해질 수 있는(perfectable)' 프로그래밍 언어라고 소개했다. 그는 Lean의 핵심 강점을 두 가지로 설명했다. 첫 번째는 의미론적 측면에서 의존 타입(dependent types)과 정리 증명 인프라를 제공한다는 점이다. 대부분의 언어에서는 함수가 항상 특정 값을 반환한다는 사실을 언어 차원에서 활용할 수 없지만, Lean에서는 'returnFive_eq_five' 같은 정리를 통해 이를 증명하고 활용할 수 있다. 두 번째는 문법적 측면에서 메타프로그래밍과 커스텀 문법을 원활하게 지원한다는 점이다. 예를 들어 틱택토 게임의 보드를 시각적 형태로 표현하는 커스텀 문법을 정의할 수 있으며, 이는 컴파일 타임에 검증된다. Singh은 PHP, Python, TypeScript 등 타입이 없던 언어들이 점차 타입을 도입하는 추세를 언급하며, 결국 의존 타입이 가장 적절한 해결책이라고 주장했다. 그는 의존 타입이 튜링 완전성처럼 모든 것을 해결할 수 있는 기반이 된다고 설명했다.