요약
Lean 4로 RealWorld 앱을 끝까지 만들 수 있었지만, 실서비스에 쓰려면 아직 조건이 붙습니다.
증명 보조기로 알려진 Lean 4를 평범한 웹 앱 개발에도 쓸 수 있는지 시험한 글입니다. 작성자는 공식 테스트가 딸린 미디엄 클론인 RealWorld를 데이터베이스부터 화면까지 Lean으로만 만들었습니다.
왜 중요한가
- 증명용으로 여겨지던 Lean 4에도 DB, 로그인, HTML 생성까지 갖춘 웹 앱을 짤 라이브러리가 생겼습니다.
- 타입과 증명으로 일부 버그를 빌드 단계에서 막을 수 있지만, 앱 전체를 설계부터 올바르게 보장하는 수준은 아닙니다.
- 작성자는 트래픽이 적고 버전을 고정하고 코드를 꼼꼼히 검토한다면 실제 사용자를 받을 만하다고 봤습니다.
핵심 내용
- 공식 API 테스트 154개를 모두 통과했고, 웹사이트 테스트는 건너뛴 65개를 뺀 74개가 통과했습니다.
- 백엔드는 1,033줄로 TypeScript(1,267줄)와 Go(1,371줄) 구현보다 짧고, 화면까지 합쳐도 약 1,600줄입니다.
- 라우트와 핸들러의 타입 불일치, 잘못된 슬러그(글 주소용 문자열), HTML 이스케이프 누락을 증명으로 막았습니다.
- 처리량은 초당 1,170~1,650건으로 Go에 크게 뒤졌고, 주원인인 런타임 버그 수정은 아직 정식 릴리스에 없습니다.
- 매달 나오는 새 버전이 패키지를 자주 깨뜨리고, 코드 대부분을 Claude Code가 써서 사람의 검토가 필요하다고 했습니다.
HN 반응
- Lean 4가 증명보다 일반 프로그래밍 언어로 더 좋다는 호평에, 어떤 용도에 좋은지 따져야 한다는 반론과 Rocq, F* 같은 대안 언급이 이어졌습니다.
- 일부 이용자는 긴 컴파일 시간, mathlib 의존, 테스트 커버리지 도구 부재를 걸림돌로 꼽았고, leanpostgres 같은 라이브러리가 생긴 것을 반기는 목소리도 있었습니다.
Lean 4가 증명뿐 아니라 일상적인 웹 앱에도 쓸 만한지 알고 싶어서, Datastar를 사용해 프론트엔드까지 포함한 RealWorld(미디엄 클론)를 직접 만들어 봤습니다. 새로 나온 라이브러리 덕분에 이제는 충분히 가능해 보입니다. 이 글은 그 경험을 정리한 것입니다.
대단한 작업이네요.
Lean4의 비밀은 사실 정말 훌륭한 프로그래밍 언어라는 점입니다. 말하자면 슈퍼 Haskell 같은 느낌이죠. 저는 증명 검증기로서보다 프로그래밍 언어로서의 Lean4가 더 좋습니다!
의존 타입은 형식 검증뿐 아니라 평범한 프로그래밍에서도 정말 훌륭합니다. 증명 검증에는 오히려 Agda를 더 선호합니다.
Rocq는 써 보신 적 있나요? 의존 타입을 한번 파 보고 싶어서요.
(> Lean4의 비밀은 사실 정말 훌륭한 프로그래밍 언어라는 점입니다)
여기선 무엇에 훌륭한지를 밝혀야 할 것 같은데요. "모든 걸 다 잘하는" 프로그래밍 언어는 없고, 다들 자기 자리가 있잖아요. (물론 Clojure와 그 후손들은 예외입니다. 당연히 모든 걸 다 잘하니까요.) 예를 들어 셸 명령어를 돌리는 용도라면 증명 중심 언어는 당연히 과할 테고, 가동 조종면이 달린 항공기 안정판을 만든다면 얘기가 달라지겠죠.
실용적으로 보이는데 저는 아직 써 보지 못한 것으로 F*(Fstar)도 있습니다.
멋지네요! 얼마 전에 웹 코드 일부를 TypeScript에서 Idris 2로 옮기는 실험을 했는데, 결과가 꽤 좋아 보였습니다.
하지만 고민 끝에 아직은 넘어가지 않기로 했습니다. 적어도 그 경우에는 코드의 일부 속성만 현실적으로 증명할 수 있었기 때문입니다. 시간을 더 들이면 더 끌어올릴 수도 있겠지만요. 그래서 순전히 실용적인 이유로 나머지 코드에는 여전히 테스트가 필요합니다. 그런데 Idris 2도 테스트와 지속적 통합(CI)은 지원하지만, 당시에는 테스트 커버리지를 측정하거나 뮤테이션 테스트를 수행할 방법이 없었습니다.
그 뒤로 누군가 Idris 2용 커버리지 도구를 만든 것 같지만, 뮤테이션 테스트 도구는 여전히 없습니다.
Lean 4에는 커버리지 관련 도구가 아직 없는 것 같습니다. Lean 4용 뮤테이션 테스트를 한다고 주장하는 도구를 하나 찾기는 했는데, 지원하는 범위가 아직 상당히 좁은 것 같습니다.
정말 반가운 소식입니다. 작년에 범용 소프트웨어 개발에 Lean을 쓸 수 있는지 알아봤는데 라이브러리 쪽이 상당히 부족하더라고요. 그래서 leanpostgres 같은 게 쓸 만하다는 소식은 엄청난 진전입니다.
공유해 주실 수 있는 성능 벤치마크가 있나요? 프로그램의 정확성을 얻는 대가로 어느 정도 감수할 만하다고 생각하지만, 핵심 비즈니스 로직에 대한 정리(theorem)가 더 많았으면 좋았겠다 싶습니다.
여기서 벤치마크 게임으로 Lean을 측정해 봤습니다: https://mech-lang.org/benchmarks/#v=1&ellipses=lean4&view=language&small=0&global=1&language=lean4&variant=lean4&languageBenchmark=nbody
저는 지금 Lean으로 언어 컴파일러를 만들고 있는데 쓰는 데는 문제없어 보여요. 다만 컴파일 시간이 끔찍하고, 프로그래밍 언어 하나 빌드하는 데 mathlib 의존성이 붙는 건 사람들에게 꽤 부담스러운 요구죠.
그래도 제 borrow checker는 건전성이 증명돼 있어서, 그게 Lean을 쓰는 이유입니다.
Lean을 쓰는 데 mathlib이 필수는 아니라고 알고 있는데요.
필수는 아니지만, borrow checker의 형식 증명에는 mathlib이 필요합니다.
실제로 의존하는 것들은 공리로 정의해 버리면 됩니다.
증명을 공개하는 건 좋은데, 언어를 빌드하는 데 왜 그게 필요한가요?
실제 동작을 하는 소프트웨어 한 벌과, 그 동작이 올바른지 증명하는 별도의 소프트웨어 한 벌을 따로 둘 수 있잖아요.
어떤 언어인가요?