最近のもやもやをつらつら書きます。プログラム関連の話。
なんていうのかな。「もっと良いプログラミング体験ができるはずなのに、現代にはまだない」という感覚、多少 type theory とかを掘った人ならみんな感じられると思う…んですよね。
例えば C/C++ で書いている「プログラム」と、Haskell/Rust で書いている「プログラム」ってかなり根底が違っていて。それは初心者が書く「プログラム」と、外部連携や将来的メンテコストを見据えて書かれた「プログラム」の違いと似たような話で。手続き型と宣言型の違いと似たような話で。
つまり how ではなく what を書いている。挙動ではなく保証を書いている。1つレイヤーが違うわけです。
それがわかってない人がぶっちゃけ現代のエンジニアの大半だとは思っていて (何故なら…概念を知らないだろうから)、まぁそれで世界は動いているのだけど、そうじゃない、ちゃんとレイヤーの上がった領域で私達はコードを書けるべきだと思うんですよね。
how は勝手に書いてくれる時代になったわけですし。私達の作業すべきポイントはそこじゃない。元々そこじゃなかったんだけど、それが陽に見えるようになってきた。
what の上で proof が書けると尚良かった。テストなんてやっている場合ではない。私達は自分の書いたプログラムが正しいことを保証する責務を負っていて、でもそれを人間や自然言語に移譲するのはおかしいこと。だから形式的証明がそこにはあるべきだった。
でも現代にはそれはなかった。根本的な理由は「界隈が分断されているから」だと思うけど、まぁ時間が掛かるものである、というのもそう。
結局そうやって、model の概念を獲得することすら無いままで人々はのさばっていて、低い層のコードをずっと書き連ねている。そのまま進んでほしくない。もう。
もちろん高いレイヤーのコードを誰でも書けるとは思っていなくて。結局技能はどんどん数学に寄っていくわけで。でもそれが相応しいことだと思う。
「形式」がわかってない人と対話ができるわけがない。それはそう。
人々は「言語」をちゃんとわからないといけない。わかってから喋れ。
…まぁ数学側の発展がまだ必要な部分はあるんだろうけど。
別に高いレイヤーの言葉を書く仕事が奪われないとも思っていない。言語を扱うのがうまい存在がそれができないわけがない。むしろそれが入ることでもっと活用の幅は広がって、仕事で人の出る幕は一切なくなるかもしれない。
でも自分がやりたいことを言葉 (自然言語とは限らないですよ) にする仕事だけは残るので、私はそれができたらいい。むしろ、今そうなっていない (how を書かなきゃいけない) ということが、単に人類の敗北であった、という感覚がある。
本当に人類は負けたんだと思う。目先の欲に。
勝つ方法も無かった。余裕がなかったから。
でもこのままだと本当に「間が全てすっぽり抜ける」から、言葉にできる範疇を今のうちに増やさなければならない。いや、もう遅いかもしれないけど。
残念な人たちが残念に過ごすことはどうやっても変えられないから (自然言語が扱えない人類がどれだけ居ることか)、それはもういいんだけど、自分くらいは救っておきたいのです。
結局モノが出るまで戯言でしかないので色々言いたくても口を噤む日々ですが、多少考えてることを書いておくのも将来的には良いことかもと思えてきました。
