Rosetta 2開発者のCameron Zwarich氏、Appleを離れLean FROに参加

• Appleで15年以上にわたり低レベルのシステムソフトウェアに携わってきたCameron Zwarich氏がLean FROに参加
• Zwarich氏はRosetta 2の作者として紹介されており、システムソフトウェアの経験がLean方面へ移った事例
• Lean FROでの重点は、Leanのコードジェネレーター改善に置かれる
• Leonardo de Moura氏はZwarich氏を優れたソフトウェア開発者として歓迎し、同氏の専門性がLeanエコシステムに影響を与えることを期待
• 今回の参加は、Leanが証明ツールを超えて実行性能やコンパイラ層まで強化しようとする流れと見ることができる

---

Cameron Zwarich氏のLean FRO参加

• Cameron Zwarich氏がLean FROに参加
• Leonardo de Moura氏はZwarich氏をRosetta 2の作者であり優れたソフトウェア開発者として歓迎
• Zwarich氏はAppleで15年以上にわたり低レベルのシステムソフトウェアを専門としてきた経歴がある

Leanで担う役割

• Lean FROでのZwarich氏の主な業務は、Leanのコードジェネレーターを改善すること
• de Moura氏は、同氏の専門性がLeanエコシステムに大きな影響を与えることを期待
• 投稿には#LeanLang、#LeanProver、#LeanFROのハッシュタグも付いている

[GN⁺]

Hacker News のコメント

• これ、私です！ここに載るとは思っていませんでしたが、Lean FROや、より広い Lean コミュニティの皆さんと一緒に Lean をより良くする仕事ができるのを楽しみにしています
  私のバックグラウンドは数学で、プロのソフトウェアエンジニアになる前から対話型定理証明器に関心があったので、これをフルタイムでできるようになったのは夢がかなったようなものです
  • 仕事用ノートPCが M4 MacBook Pro なので、Rosetta の美しさには本当にありがたみを感じます
    LinkedIn を見ると、2009年から Apple にいて、途中で Mozilla に1年いた以外はずっと Apple だったようですね。Waterloo の純粋数学の大学院出身というのも見ましたし、個人的には Waterloo はわが国最高の数学／コンピュータサイエンス校だと思っているので、40代になった今でも受け入れてもらえるなら迷わず行くと思います
    どういう経緯で Rosetta 2 プロジェクトに参加することになったのか気になります。大学院の論文も確認してみましたが、https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... コンパイラ理論とは関係がありそうには見えませんでした
    私も以前は数学を学んでいましたが、優秀な学生ではなく、統計学をやっていて、冗談めかして数学の一部ではないと言ったりしていたので、本格的な代数学の授業は受けておらず、その論文もまったく理解できません
  • Rosetta 2 は、これまで見てきたものの中でも屈指の、技術的に印象的な成果物です。DynamoRIO でかなり深くバイナリ変換に取り組んだことがありますが、それでも Rosetta 2 はいまだに魔法のように感じます
  • 本当に Rosetta 2 のあの作者なのですか？チーム規模はどれくらいで、ご自身の役割は何だったのか気になります
    Rosetta 2 は驚異的ですが、もしこれがたった一人で作られた仕事なら、本当に驚きです
  • ディスアセンブリ、システムコール、x86/64 アセンブラについて、おすすめの本はありますか？
    Rosetta ほど高度なものを作るには何を知っている必要があるのか気になります
    各ホスト／ゲストシステムのシステムコールを、信頼できる抽象レイヤーとして再実装してテストしたのではないかと推測していますが、理解をはるかに超える部分があまりにも多いです
    独自のアセンブラデバッガも作ったのでしょうか？作業中にどんなツールを使ったのか、Ghidra や Binary Ninja のようなリバースエンジニアリングツールが役に立ったのかも気になります
  • 2009年から少なくとも FAANG にいたのなら、引退したり、1〜2年ほどサバティカルを取ったりしたことがあるのか気になります
    それだけなら、引退しても年収に近い水準の不労所得で暮らせるくらい稼いでいた可能性がありますし、税制面でもずっと有利だったはずです
    意思決定がどう形作られたのか、純粋に気になります。FAANG、特に Apple が満足できる場所だったならもちろん問題ありませんし、Blind でそういう例を多く見ているので、非合理的なほどの経済的不安があるのかも気になります
• 以前の議論で Gary Davidian という名前が出ていましたが、彼も Apple のアーキテクチャ移行で、当初はほぼ一人で驚くべき仕事をしていました。Computer History Museum のアーカイブにインタビューがあります
  https://news.ycombinator.com/item?id=28914208
  https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
  • Wiki を見ると、David のエミュレータは解釈実行を使っていたようで、Eric のものは動的再コンパイルを使っているとされており、Connectix 側はさらに高速なので、より多くの最適化が入っていたようです
    ソースコードを探してみましたが、何も見つかりませんでした
• LinkedIn の戻るボタンがおかしいです。戻るを押しても HN に戻らず、LinkedIn のホームページに移動します
  • おかしいのではなく、気持ち悪い挙動です。戻るは前のページに戻るべきです
• Lean FRO とは何ですか？
  • https://lean-fro.org/about/
  • Lean は現時点ではニッチなプログラミング言語であり、証明支援器でもあります
    証明支援器は基本的に数学的証明を構成するためのツールで、コンパイラがプログラムの型を検証するように、証明が正しいかを検証します
    私の理解では、Curry と Howard が発見したように、特定の制約を持つ通常のプログラミング言語も証明支援器に対応します。ここでいう制約とは、Java と比べて Rust が特定の規則に従うよう強制する、というのに近い感覚です
  • 組織の背景: https://en.m.wikipedia.org/wiki/Convergent_Research
    彼らの証明支援器／プログラミング言語: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
  • https://lean-lang.org/lean4/doc/
  • 「Lean 証明支援器におけるスケーラビリティ、ユーザビリティ、証明（数学）の自動化の課題に取り組むことを目標としている」
• Lean の非営利組織は、どのように資金を調達して、これほど優れた開発者たちを雇えるのでしょうか？一般的にこうした仕組みがどう回っているのか気になります
• Apple があちこちで人材流出に見舞われているように見えます。今のように雇用市場が不確実な時期に、人々を辞めさせるようなことが内部で何か起きているのか気になります
  • 20番目の100万ドルは19番目の100万ドルほど大きくは感じられませんし、保有株の配当で年収の2倍を稼げるようになると、単にもっと面白いことをしてはいけない理由があるのかと考えるようになります
  • ただクールなことをしたい人もいて、そうできる余裕もあります。Rosetta 2 はすでにリリースされ、終わったプロジェクトです
  • 1985年にこの言葉を言っていても正しかったでしょう。才能ある人々には選択肢があります
  • 根拠が必要です
    長く勤めた人が辞めることは常にありますし、提示されたポジションがなくても、結局どんな仕事も古びて感じられるものです