人間ではなく「機械」が書くために設計された言語「Vera」が登場！

人間がコーディングする時代は終わるのか？「Vera」は、人間による可読性ではなく、機械が効率的に記述・最適化することを最優先に設計された、次世代のプログラミング言語です。AIによる自動生成コードの未来を切り拓く注目のプロジェクトです。

ゼロ除算は実行時エラーではなく、型エラーです。コンパイラがすべての呼び出し箇所をチェックして、除数がゼロではないことを証明します。

このあたり、もうちょっと詳しく教えて。

名前の代わりに構造的な参照を使うことが、LLMによるコード生成の精度向上につながるという証拠はあるの？単に複雑にしてるだけにしか思えないんだけど。

私のプロジェクトじゃないけど、自分の仕事で考えていた重要なアイデアがいくつか含まれていたから共有したんだ。特にエフェクト型システムは、LLMと相性が抜群。実行前にプログラムの能力を極めて正確に推論できるからね（要するに、型システムを能力証明に使っている）。これにより、エージェントが生成したコードを信用しやすくなるし（例えばIOができないと保証できる）、もし特定の能力が必要なコードならサンドボックスで動かすといった判断もできる。ランタイムの実装次第ではあるけど、こういう言語設計は、エージェントがエージェントを作るような複雑なメタシステムにとってもより安全な基盤になる。まあ、Veraがどこまで対応できるかは未知数だけどね。

ただ、変数名を排除するという設計判断には少し懐疑的かな。直感的じゃない気がするし、そのあたりの実証データを見てみたい。むしろ逆で、変数名があったほうがLLMに有用な局所的セマンティクスを与えられると思うんだけど。

実証研究によると、モデルは誤解を招く名前の選択、不適切な名前の再利用、どの名前がどの値を指しているかの見失いといった、名前に関連するエラーに特に弱い。

Veraの考え方は何かを見落としている気がするな。経験上、LLMはメンタルモデルを頭の中で構築する必要が少ないコードの方がうまく書ける。ページ上に情報が全部出ている方がいいんだ。

Go言語なら隠蔽が少なくて全部テキストとして見えるから、LLMはすごく優秀。Javaも似たような感じ。でもHaskellやErlangとなるとかなり厳しい。そういう言語はもっと高度なメンタルモデルが必要だからね。

Veraの場合、名前をなくすことでモデルが本来持てるはずの重要な情報を取り除いてしまい、代わりに引数のスタックを頭の中でモデル化させるような負荷をかけているんじゃないかな。

変数名はありません。@Int.0が直近のIntバインディングで、@Int.1はその前です。

もうここでついていけない。プログラミングに変数が存在するのには理由があって、それは意味をセマンティクスとして伝えるためだよ。人間が書こうがLLMが書こうが、その点は重要だろ。

（決定可能性のための）Hindley-Milner ＋（リソース管理のための）線形型 ＋（不変条件を軽く主張するための）洗練型 ＋（副作用のあるコードを追跡するための）区切られた継続ベースのエフェクト ＋（コード変更、ドキュメント、テストをまとめるための）Unisonスタイルのコンテンツアドレス指定。これらを組み合わせたら、LLMにとって最高に相性のいい言語になりそう。

名前がないという設計は、LLMコーディングエージェントがなぜ成功しているのかという根本的な理解が欠けている気がする。このプロジェクトが実用的で機能するのか、疑わしく思えてくるよ。

これは完全にアプローチを間違えている。LLMはトレーニングデータに豊富に含まれる「既知のプログラミング言語」を書くのは得意だけど、見たこともないような言語を書くのは苦手なんだ。結局、プログラミング言語のマニュアルと大量のサンプルコードをプロンプトのたびに含めなきゃいけないことになる。

LLMは変数名の扱いでミスをしやすいっていう主張、正直よくわからないな。

私と作者の間で、複雑なコードベースやビジネスロジックにおけるLLMの能力について、経験がかなり食い違っているみたいだ。

私の観測では、変数やメソッドに明示的で詳細な名前がついている方がLLMは遥かにうまく動く。それがLLMの迷走を防いで混乱を最小限にする最善の方法だし、次点は明示的なコメントやインラインドキュメントだよ。

コードベースの名前が適当でドキュメントも貧弱だと、モデルは「それが何であるか」を推論するはめになって、結局（間違った）結論に達する。トークンの無駄だし時間の無駄。

この哲学のズレは、ツールをどう見ているかという根本的な違いから来ているのかもしれない。

私はマシンを信用していないから結果をレビューするけど、変数に名前がなかったらその作業は格段に難しくなる。もし「あとは神に任せた！」みたいなスタンスで開発しているなら、名前なんてどうでもいいのかもしれないけどね。

「## Why（なぜ作ったか）」のセクション、すごくいいね！すべてのリポジトリにあるべきだよ :-)