"수학 증명 언어로 웹 풀스택을 만든다고?" Lean 4로 실제 웹 앱 만들어본 개발자

요약 수학적 정리 증명 도구(Proof Assistant)로 주로 알려진 함수형 프로그래밍 언어 Lean 4를 활용해 풀스택 웹 애플리케이션인 'RealWorld'를 구현한 개발자의 도전기가 공유되었습니다. RealWorld는 Medium 스타일의 블로그 플랫폼으로, 공식 API 및 웹사이트 테스트 스위트를 갖추고 있어 다양한 언어와 프레임워크의 완성도를 검증하는 대표적인 레퍼런스 앱입니다. 작성자는 논문 형식의 위트 있는 구조를 차용해 'Lean 4로 RealWorld 앱을 만들 수 있는가'를 '정리(Theorem)'로 두고 구현 과정을 증명하듯 풀어냈습니다. Lean 4의 표준 라이브러리에 최근 추가된 Std.Http 서버 모듈을 기반으로 라우팅 테이블을 설계하고, PostgreSQL 전용 라이브러리를 연결해 데이터베이스 쿼리를 처리했습니다. 프론트엔드의 경우 별도의 복잡한 빌드 단계 없이 가벼운 하이퍼미디어 라이브러리인 Datastar와 서버 렌더링(lean-html)을 조합해 구현했습니다. 그 결과 공식 API 테스트와 브라우저 기반 웹사이트 테스트를 모두 통과했습니다. 특히 Lean 4로 작성된 백엔드 코드는 총 1,033줄에 불과해 TypeScript(1,267줄), Go(1,371줄), C#(2,396줄) 등 비교 대상 언어들보다 더 짧고 간결한 코드량을 기록했습니다. 다만 개발자는 Lean 4 웹 생태계가 아직 초기 단계라 프로덕션 도입에는 처리량 한계 등 일부 과제가 남아있다고 덧붙였습니다.