Nvidiaが提案する！C言語を使わない未来とは？
引用元：https://news.ycombinator.com/item?id=42998383
SPARKを使ったらしいよ。SPARKはAda言語に基づいた正式なプログラミング言語で、高い信頼性が求められるソフトウェアを開発するためのもの。安全性やセキュリティが重要なアプリケーションの開発を助けてくれる。
記事の最初を読まない人には朗報だね！正式確認は特に並行処理が多い環境で効果的なんだ。Nvidiaが使うのも納得。パイロットプロジェクトの成功も気になるところだ。
SPARKの開発がもっと活発だといいんだけど、10年間ほとんど手が加わってない。SPARKはRustよりも多くの安全策や保証を提供していて、コンパイル時に処理されるからね。
Nvidiaが使ったのは、一般的なSPARKのバージョンじゃなくて、SPARK Proっていう商用版だったらしい。
SPARKは誰でも使えるオープンソース。NvidiaはAdacoreのプロサポートを選んだけど、実際にはGNATコンパイラの一部として使われているよ。
AdaCoreのプロサポートは新しいリリースが含まれていて、問題があった場合も安心。ただ、無料版もそこそこ最近のバージョンが手に入るから、ある程度のサポートもあるよ。
SPARKは宇宙船プログラミングでも支持されているよ。正式な検証と安全機能があるからね。
もしAdaCoreがカールブラケット構文を受け入れるコンパイラを本気で作ったら、新しいユーザーが倍増すると思う。ただ、表面的なものに影響される人が多いのも事実だね。
Adaとは関係ないけど、Dafnyっていう正式な仕様と検証を統合したプログラミング言語もあるよ。複数の言語にコードを生成できるのがいいね。
VHDLっぽい構文は意外にいいよ。驚くべき現代的な機能もあるし。
誰もが’{’をBEGINに、’}’をENDにマッピングするプリプロセッサを作るのを妨げるものはないよ。
Pascalの派生言語のModula-2、Oberon、Lua、AdaはIFやFOR、WHILEなどにBEGINを必要としないから、構文がずっとスッキリしてるよ。
文法の実装はプログラミング言語の普及のほんの0.1％に過ぎない。g++に非constを明示的に追加するのは簡単。でも、意味がない。
Rustを止めたいのは分かるけど、言語の採用には大きなnpmクローンの有無が鍵だと思うよ。
Alireは2018年から存在していて、GitHubにある最古のリリースは0.4だよ。
現行の構文はおかしいから、改善すべきだと思う。
おかしいってことはないけど、時代遅れだね。Adaの構文はPascalと同じ系譜から来ていて、80年代にはCと同じくらい人気だったんだよ。
確かにそうだけど、構文が消えた理由ではないよ。最近プログラミングを始めた人にはカッコいい中括弧の言語にしか慣れてないから理解できないかもしれないけど、だからと言っておかしいわけじゃない。
Pascalのオブジェクトコードはランタイム範囲チェックがあれば、Cより遅くなるかもね。Pascalの文字列は静的に制限されてたり、範囲情報があったりするけど、Cはそうじゃないからバッファオーバーフローが発生しやすいんだよね。Adaはメモリ安全性を重視して、特に並行性の安全性や形式検査と組み合わせることで良い結果を出してる。clang/llvmもメモリ安全性向上に向けて進展してるし、CやC++が1980年代に追いつければいいね。
Pascalの派生言語であるModula-2やOberon、Lua、AdaはIFやFOR、WHILE、LOOP、CASE文でBEGINが不要だから、文法がPascalよりもすっきりしてるよ。
記事ではNvidiaのスタックのどの部分がSPARKを使ってるのか触れてないね。Nvidiaは約3万人的な大企業で、”開発者は50人以上トレーニング済みで、SPARKで実装されたコンポーネントもある”って言っても、あまり信頼感が湧かないな。個人的には、形式検証の現実的な道は、AIの助けで面倒な部分を自動化することだと思うんだ。変な書き方にこだわる必要はない。 AIによるコード生成は、Nvidiaみたいな並行性要件のあるところでは、逆に見つけにくいバグを増やすかもね。のんきにタブ補完でコードを書いちゃうと。だけど、形式的に検証可能なプログラムのためのAIコード生成は良いかも。未来のプログラミング言語に期待だね。 Rustの件だけど、借用チェッカーはAIには無理じゃないかな。コードの暗黙のプロパティや全体の構造に関しては多くのことが分かっていないと思う。 NvidiaがRustよりSPARKを選んだのは、形式検証のためじゃなくて、もっと発展してて、安全性が高いからって話もあるみたい。Adaはレジスタやネットワークパケットのモデリングも得意だしね。個人的にはSPARKのgnat proveを活用したAIを考えるけど、他は使わないかな。 パケットモデリングの例として、ビットパッキングされたタグ付けされたユニオンの複雑なパケットモデリングの例を紹介するね。多分、他の言語ではこんなに簡単に宣言できるものはないと思う。 Sorry to say but AI can’t figure out the borrow checker. I’d speculate it does poor on a lot of things that are sort of implicit in the code / properties of the grand structure rather than incremental text things. AIツールはあまり使わないけど、最近Rustで試したとき、借用チェックのエラーは問題にはならなかったよ。確かにLLMは理解できてないけど、借用に対して考えるべきことはそんなに多くもないと思う。 実際に、AIによるコードレビューツールが新しいメソッドへの切り替えを提案して、両方ともそれが良いアイデアだと思ったんだけど、実際にはAndroidのactivityのonCreate()には使えないメソッドだったんだ。直接関係ないActivityに影響を与えて、問題が起きた。こういうのは表現力のある型システムなら簡単に見抜けたのに、LLMはわからないんだ。 AIによるコード生成が形式的に検証可能なプログラムに役立つかも？検証が実際には面倒なのは確かだけど、最近のモデルはその助けになるはず。 o3-miniを使って8×8ビット整数の加算を検証したけど、あまり感心しなかった。エンドiannessやケリーの問題なんて言われたけど、実際は違ったし、提案された反証も役に立たなかった。形式的検証には、決定的で明確なプロセスが大事だと思う。 AIによるコーディングは主流の問題でないと結果がイマイチ。PHPやPythonだとまあまあだけど、PostGISの質問をすると訳のわからない回答が返ってくる。ADA/Sparkや形式的検証の分野は小さすぎて、AIが訓練できない気がする。 今のLLMによるコーディングは、自動化されたStack Overflowのコピー＆ペーストみたいなもので、シンプルなものにはまあまあだけど、コードを根本から考える能力はないし、見た目は良いけど動かないものを作りやすい。 初めてLLMにコードのスニペットをお願いしてみたんだけど、コンパイルは通ったけど実行すると何も動かないって結果だった。3つ目のAPIコールでエラーが出たし、期待通りにはならなかった。 OPはAIが形式的に検証できるコードを生成すると言ってるのか、AIが検証してると言ってるのか、ちょっと違うかもしれないけど、前者だと思ってた。 形式的検証の段階まで来ているなら、かなり細心にコードを書くはずだから、AIは慎重に使うことになると思う。 Nvidiaってソフトウェア会社じゃなくて半導体会社だよね。30,000人の社員には全員がソフトウェア開発にいるわけじゃないからね。AIにはあまり期待してない。AIアシスタントが正確でない限り、細かいエラーを人間が見つけないと意味ないし。Cコードを検証するツールはあるけど、ゼロからのプロジェクトは高階の正式な言語で実装して検証した方が良さそう。 記事ではNvidiaのどの部分がSPARKを使ってるかは触れてないね。関連のケーススタディには3つの例が挙げられてるけど、全体のGPUファームウェアの画像の画像認証と整合性チェック、BootROMとセキュアモニタのファームウェア、埋め込みOSの隔離カーネルの正式検証されたコンポーネントがあるよ。特に、小さいコードベースでSPARKの強い型付けやランタイムエラーのないことが大きなメリットになる。 Nvidiaのセキュリティチームが主導してるのが分かるね。エンジニア50人はこの規模の会社なら妥当だと思うよ。 これからは実際の「コード」を書くんじゃなくて、総合テストを考えて、それを元にコードが生成される時代になると思う。アセンブリからCに移ったのと同じようにさ。 AIには大きな課題があると思う。機械学習は、すべてのテストケースをクリアする解決策を見つけるのが得意だけど、意図したことをしないことが多いからね。 包括的なテストを書くのが一番の弱点だと思う。安い場所に開発をアウトソーシングして、結果に対して受け入れテストを行うのと同じだよ。それじゃ飛行機は作れないよ。 人間は全てのケースをカバーするテストを書くのが苦手だと思う。テストを誰がテストするの？ AIがプログラミング言語のセキュリティに大きな影響を与えると思うし、多くのパラダイムが変わるはずだよ。 フォーマルな検証はセキュリティが最も重要なコードに使われるから、50人も開発者がいれば十分だよ。 他の99.9％の会社がSPARKを使ってないのに比べればね。テストや静的解析だけのレベルだよ。 AAAゲームが出るたびにカスタム調整パッチを出してるんじゃないの？GeForce Experienceは新しいドライバーをインストールさせるための甘いトリックだよ。 彼らの話をチラッと見たけど、NVIDIAの安全性に関する提言をする外部のコンサルタント会社だね。言語を完全に変える姿勢にはちょっと違和感があるな。CUDAはC/C++ベースだし、大規模プロジェクトでは弱点が見つかる可能性もあるよ。 ＞”外部のコンサルタント会社だね。”これは顧客であるNVIDIAの数年に渡るエンジニアリング作業のマーケティング事例だよ。NVIDIAは今やSPARKを使用して、画像の認証やGPUファームウェアの整合性チェックを行ってるんだ。 彼らの仕事は低レベルのファームウェアに注力してるようで、CUDAや計算には関係ないみたいだね。ライブラリが少ない分、論理的な証明や自動化が進みやすいんじゃないかな。 そのどこが取りにくいの？文法に関することならPythonでどう説明するの？ おもにCでプログラム書いてAdaライブラリ呼ぶか、Adaで書いてCライブラリ呼ぶかって話だね。これ、C/RustやC/Pascal、Rust/Pythonでも同じようなこと言えるよね。 俺のメインプログラムはC++でSTLのおかげで便利なんだよ。Vectorやunique_ptrみたいな面倒なもんがあって、CよりC++がいいんだ。 Cライブラリ呼ぶときと同じで、STLオブジェクトをプレーンCオブジェクトに変換して渡して、戻ってきたらデシリアライズする感じ。コールバックが必要なら例外を捕まえてエラーコード返せばいいだけ。ほんと、他の言語との相互運用性とはそんなに変わらないよ。 C++コンパイラの小さなパートを実行環境に組み込んで、C++と深くやり取りできる言語がいくつかあるよ。 相互運用のためのシリアライズ/デシリアライズで性能が落ちるから、言語自体が実用的じゃなくなるんだよね。 でも、コールごとのオーバーヘッドがほんの少しの命令数なら、文脈によってはそんなに悪くないかも。大きなバッファーをコピーするのが問題だけど、普通は避けられるはず。 俺はAdaが問題とは思わないよ。RustやGo、Swift、Zig使っても同じ問題が出ると思う。C++の機能を多用すると、他の言語との相互運用性が難しくなる。 GCC使えば、クラスレベルでの相互運用がちょっと楽になるよ。 ほんとだよ。C以外の言語はC以外のものとの相互運用性が悪い気がする。C++はRustの借用チェッカーと相性悪いし、Goもいろいろ問題がある。DはC++サポートしてるけど、どうなのかは詳しく知らない。 Cと古典的な3世代言語の相互運用はそこまで難しくないよ。Cの機能セットとだいたい同じだから。C++やGo、Rust、Swift、Adaみたいな言語は複雑な機能が多いから、使うと相互運用が難しくなる。 俺は15年以上AdaからCやC++のコード呼び出してるし、逆もやってきたよ。Pythonとも行き来してるし、Javaを介してJNIで呼び出したりも。Postgresの拡張をAdaで書いたこともあるけど、可能なのは確かだよ。もっとコメントを表示（1）
もっとコメントを表示（2）
