Lean 4로 RealWorld 앱을 만들어봤다

I built the RealWorld app in Lean 4

Lean 4로 RealWorld 레퍼런스 앱을 서버부터 프런트엔드까지 전부 구현했다. Lean 표준 라이브러리의 HTTP 서버와 Paul Butcher의 라이브러리들, Datastar 기반 상호작용을 사용했고, API와 웹사이트 테스트 스위트를 모두 통과했다. 백엔드 코드는 1,033줄로 비교한 네 구현 중 가장 짧다. 하지만 HTTP 서버 성능 한계와 잦은 버전 변경, AI가 작성한 코드의 검증 문제 등 프로덕션 적용에는 조건이 따른다.