今現在おれは仕事をしておらず、こどおじニート生活を送っているが、 もし、またシャバでソフトウェア開発をするとしたらそれはどういう開発になるだろうかと妄想したりはしている。

AIの発展は凄まじく、海外ではソフトウェア開発に限らず様々な仕奪がゴリゴリに奪われてきていると聞くし、 日本でも今後のAIの発展を見込んだ整理解雇が進んできている。 その発展は、一説には2027年にはAGIが誕生すると言われていて、 その後AGIによってASIが秒で実現されるという見込みがある。

そのような高度なAIが誕生してしまった場合、 我々人間は完全に「ギュられる」わけであるが、 その前に、人間がAIを使いこなして生産性を爆上げするフェイズが長く続く可能性もある。

その場合について考えると、 ソフトウェア開発においては、 超少数の人間がAIにコードを書かせてソフトウェア開発を行う という形になるはずであり、 もしそうであれば、そのような形態の開発に合うプログラミング言語とはどのようなものであろうか と考えてみるのも面白い。

結果、最近のおれはブログもユーチューブも更新を止めて、Lean4の調査をしていた。 Lean4は、関数型言語でもあり、定理証明器でもあるプログラミング言語である。

なぜLean4に注目しているかというと、 結局、そのような世界においては、AIが書いてきたコードが信頼出来るかを どれだけ広く機械的にチェック出来るかが鍵になると思うからだ。 また、型によってソフトウェアの動作を出来るだけ定義出来た方が、 AIとの間でのコミュニケーションにも齟齬も生まれにくいだろう。 他には、似たような言語だがIdris2にも注目している。

一般的には、言語を選定するとき、人員の採用のしやすさなども 考慮する必要があるが、相手がAIならばこれは関係ない。 また、現状のエコシステムの未発達も、大した問題にはならないと思う。

こうした新しい言語を調査しているもう１つの理由は、 おれが現状一番得意な言語は何かというと それはたぶんRustということになってしまうと思うのだが、 この言語は本当に面白くない。あまりに優れており、何でも出来てしまう。 Rustを書いている限り、おれは無敵だろう。 しかしこんな超絶コンフォートゾーンにいては概念的成長はないわけであり、 いっそLean4くらい先鋭的な言語で自分を縛ってしまい何も出来なくなって死んでしまった方がいい。

ただこのLean4、信じられないくらい難しい。 宇宙レベルがどうとか、おそらく、数学科出身でないとすんなりは理解出来ないのではなかろうか。 頭に自信のある人はチャレンジしてみてほしい。