Lean 4로 만든 Medium형 참고 앱 RealWorld가 공식 API·웹사이트 테스트를 모두 통과했다. 다만 실제 서비스에 쓰려면 트래픽이 적고 도구 버전을 고정해야 하며, 사람이 코드를 검토해야 한다는 조건이 따른다.
Lean 4는 함수형 프로그래밍 언어이자 증명 보조기다. 최근 표준 라이브러리에 HTTP 서버가 추가됐고, 커뮤니티도 데이터베이스 드라이버와 암호화, HTML 렌더링 라이브러리를 만들고 있다. 이 구현은 프런트엔드까지 Lean으로 작성했으며, 상호작용에는 datastar-lean을 사용했다. RealWorld 프로젝트는 API와 웹사이트 공식 테스트 모음을 제공한다. 구현 코드는 GitHub 저장소에서 볼 수 있다.
앱은 Lean 표준 라이브러리의 Std.Http 서버와 lean-routing을 사용한다. 데이터는 Postgres에 저장하고 leanpostgres로 연결한다. SQL 쿼리에 사용자 입력을 매개변수로 전달해 입력값이 SQL로 실행되지 않도록 하며, 데이터베이스 스키마는 leanmigrate로 서버 시작 시 적용한다.
페이지는 lean-html로 서버에서 렌더링한다. Datastar가 버튼 클릭에 따라 요청을 보내고 서버 응답으로 페이지를 갱신하므로 별도의 프런트엔드 빌드 단계는 없다. 구현에는 JSON용 lean-json, 비밀번호 해싱용 lean-libcrypto, 로그인 토큰용 lean-jose, CORS·쿠키·정적 파일 처리를 위한 lean-middleware도 쓰였다. Datastar의 Lean SDK인 datastar-lean은 Carlo Hamalainen과 앱 구현자가 함께 유지 관리한다.
이 구현의 백엔드는 1,033줄로, 비교한 네 구현 가운데 가장 짧다. TypeScript 구현은 1,267줄, Go는 1,371줄, C#은 2,396줄이다. 사용한 라이브러리 11개 중 10개는 Paul Butcher가 만들었으며, Claude Code와 앱 구현자는 개발 과정에서 라이브러리 여섯 개에 수정 사항을 보탰다. 이 수치는 코드 규모를 비교한 것이며, 품질이나 성능을 입증하지는 않는다.
실제 서비스에 적용할 때의 조건
글은 Lean의 HTTP 서버가 프로세스당 초당 수천 건 정도의 요청에서 한계에 이르며, 주된 원인은 Lean 런타임의 버그라고 설명한다. 해당 버그는 수정됐지만 아직 릴리스되지 않은 상태다. Lean은 매달 새 버전을 내고 라이브러리가 새 버전에서 깨지는 경우도 잦다. 따라서 작은 사이트라면 트래픽을 적게 유지하고 도구 체인 버전을 고정할 때 이런 문제가 큰 장애가 되지 않을 수 있다. 앱은 요청 사이에 상태를 보관하지 않아 여러 인스턴스로 실행할 수도 있다. HTTP 서버 관련 설명은 원문 주석, 버전 안정성 설명은 원문 주석에 있다.
또 다른 주의점은 코드의 검토 이력이다. 앱 코드 대부분은 Claude Code가 지시에 따라 작성했고, 라이브러리 상당수도 같은 방식으로 만들어졌다. 코드와 라이브러리가 만들어진 지 몇 달밖에 되지 않았고, 대부분 기여자는 한두 명뿐이다. 따라서 실제 사용에서 발견될 버그가 남아 있을 가능성이 있다. 기여자 정보는 원문 주석에서 확인할 수 있다.
Lean은 타입과 정리를 검사하지만, 정리가 필요한 동작을 제대로 설명하는지까지 확인하지는 않는다. Dan Luu가 코딩 에이전트에 Zstd 압축을 Lean 4로 구현하게 했을 때, 에이전트는 버그가 생기기 쉬운 코드 대신 산술 사실을 주로 증명했다. 이 증명은 코드의 정확성을 높이지 못했다는 설명이다. 사례에 대한 원문 주석과 정리의 뜻을 AI가 풀어 쓴 뒤 원래 의도와 비교하는 도구 claimcheck, 관련 주석도 소개한다. 도구는 검토를 도울 뿐 직접 읽는 일을 대신하지 않는다. C 라이브러리 바인딩은 Lean이 C 코드를 검사할 수 없으므로 특히 주의해야 한다.
증명으로 보장하는 범위와 한계
RealWorld의 명세는 OpenAPI 파일과 테스트 모음으로 구성된다. OpenAPI는 엔드포인트, 입력 필드, 상태 코드 같은 형식은 구체적으로 정하지만 실제 동작은 영어로만 설명한다. 테스트도 작성된 사례만 확인한다. 따라서 이 앱은 명세에서 코드를 단계별로 유도해 각 단계를 증명하는 ‘구성에 의한 정확성’을 달성하지 못했다. 앱을 먼저 만들고 나중에 테스트했으며, 대신 일부 속성을 증명했다.
예를 들어 경로에 지정된 타입과 처리기 타입이 맞지 않으면 컴파일되지 않는다. 댓글 ID가 정수로 정해져 있는데 처리기가 문자열을 받도록 작성하면 실행 전에 오류가 난다. 다만 경로 표를 OpenAPI 파일에서 자동 생성하지 않고 손으로 옮겼으므로, 그 과정의 불일치 가능성은 남는다.
슬러그는 더 좁은 범위에서 구성에 의한 정확성을 보여준다. 앱은 소문자나 숫자로 이뤄진 한 글자, 또는 그런 글자 앞에 다른 글자나 하이픈이 붙는 형태만 유효하다고 정의한다. 이 규칙은 빈 슬러그, 양 끝의 하이픈, 연속된 하이픈을 막는다. 슬러그를 저장하는 함수는 유효성 증명이 붙은 타입만 받는다. 제목을 슬러그로 바꾸는 함수도 어떤 제목을 입력받더라도 결과가 유효하다는 증명을 포함한다. 관련 증명은 코드 약 10줄에 대해 약 40줄이며, 글은 이를 무작위 제목 몇천 개를 확인하는 속성 기반 테스트와 달리 모든 제목에 적용되는 보장으로 설명한다. 관련 주석.
또한 Node.unsafeRaw를 호출하지 않는 한 사용자가 입력한 문자는 페이지에 표시되기 전에 이스케이프된다는 정리를 제시한다. lean-html의 함수는 텍스트를 이스케이프하며, 그 결과에 <, > 또는 "가 남지 않는다는 점을 Lean이 검사한다. RealWorld 웹사이트 테스트는 크로스사이트 스크립팅을 검사하지만 API와 페이지를 함께 제공하는 앱에는 해당 테스트를 건너뛴다. 이 구현에서는 해당 보장을 증명이 뒷받침한다.
따라서 앱 전체가 구성에 의해 정확하다고 볼 수는 없다. RealWorld의 동작을 Lean으로 명세하고, 앱을 그 명세에서 유도하려면 SQL 모델과 C 라이브러리, Std.Http에 대한 증명도 필요하다. 현재 이 방법을 끝까지 적용한 부분은 슬러그뿐이다. 테스트 통과에 관한 원문 주석, 코드 줄 수 비교 주석, 라이브러리 수정 주석, 증명 관련 주석에서 세부 내용을 볼 수 있다. 앱과 두 테스트 모음을 실행하는 방법은 저장소에 안내돼 있다.
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요