Lasm - Lean 4로 검증된 웹앱을 Node·서버리스·엣지에 배포

Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge

▲ 33lastmjs20 HN 토론

Lasm은 Lean 4 프로그램을 WebAssembly로 사전 컴파일해 하나의 코드베이스로 Node 서버, 서버리스 함수, 엣지 런타임, 브라우저 앱까지 만들 수 있게 해주는 도구입니다. Lean이기에 배포하는 코드의 속성을 수학적으로 증명할 수 있다는 점이 핵심입니다. 대표 예제인 Conduit은 RealWorld 앱을 Lean으로 구현하고 117개의 정리를 증명했으며, 공식 API·E2E 테스트 스위트도 통과합니다. npm으로 설치하고 Node만 있으면 바로 시작할 수 있어, 타입 안전성을 넘어 '증명된 안전성'을 원하는 개발자에게 매력적인 선택입니다.

Lean이기에 배포하는 코드의 속성을 증명할 수 있습니다. 대표 예제 Conduit은 117개의 정리를 증명한 RealWorld 앱입니다.
원문 읽기 →HN 토론RSS

HN 토론

20
  1. alexhixon

    흥미롭네요! 프론트엔드 관련 증명을 더 보고 싶었어요. 예를 들어 동작에 대한 증명은 있지만 레이아웃이나 디자인에 대한 증명은 하나도 없잖아요.

  2. orsorna

    > 저는 소프트웨어 엔지니어링에 중점을 둔 에이전틱 엔지니어입니다

    이건 좀 이상하네요. 자신을 소프트웨어 엔지니어이면서... 에이전틱 엔지니어링 같은 걸 중점으로 둔다고 생각하진 않으실 텐데요? 배경이 어떻게 되세요?

  3. sroerick

    이거 굉장히 흥미롭다고 생각해요. 그런데 웹사이트를 만들 때 대체 무엇을 명세하는 건가요?

    이건 새로운 "테스트 주도 개발" 같은 느낌이에요. 완전히 좋은 아이디어긴 한데, 정작 웹앱을 만드는 실제 과정에서는 그다지 유용하지 않죠. 대부분의 실패 모드는 이상한 CSS나 JS, 아니면 서버 문제니까요.

    그래도 제가 틀렸다는 게 증명되면 좋겠네요.

이 날의 다른 글

2026-10-30