Lasm - Lean 4で検証済みWebアプリをNode/serverless/edgeにコンパイル
Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Lasmは、Lean 4プログラムをWebAssemblyに事前コンパイルし、Nodeサーバー、サーバーレス関数、エッジ関数、WASIモジュール、ブラウザアプリとして展開できるツールです。コードの性質を数学的に証明できるため、高い信頼性が求められるアプリケーションに最適です。フラッグシップ例のConduitは117の定理が証明されたRealWorldアプリで、APIとフロントエンドがLeanで書かれています。npmからインストールでき、Node（またはBun/Deno）があればすぐに始められます。
Leanで書かれているため、デプロイするコードの性質を証明できます。
HNでの議論
20- alexhixon
面白い！フロントエンドに関する証明をもっと見てみたかったですね。例えば、挙動に関する証明はあるけれど、レイアウトやデザインに関する証明は一つもないですよね。
- orsorna
> 私はソフトウェアエンジニアリングを重視するエージェント型エンジニアです
これは奇妙ですね。自分を「……エージェント型エンジニアリングを重視するソフトウェアエンジニア」とか、そういうふうには考えないんですか？ご経歴はどんな感じなんですか？
- sroerick
これはとても面白いと思いますが、ウェブサイトを構築するときに一体何を仕様として定義しているんですか？
これは新しい「テスト駆動開発」のような気がします。完全に良いアイデアではあるけれど、ウェブアプリを実際に構築するプロセスではあまり役に立たないんじゃないかと。というのも、失敗の原因のほとんどは奇妙なCSSやJS、サーバーの問題ですからね。
ただ、間違っていると証明してくれるなら嬉しいです。