なるほど。
ちょっと恥ずかしい感じの。
JetBrains境に入ったんですね。
JetBrainsのいいところは、どの言語を書いていてもJetBrains IDが大体あるってことなんですよ。
パールを除いてですけど。
すごいですよね。
大体ある。
アップコードのサポート終了してしまうっていう例はありつつも、
大体サポートしてましたからね。
それで言って、その拡張機能とかってのは大体どれでも通用するし、
カラースキムとかも使い回しが効くしっていうのがあって、
それでもうずっとJetBrainsでええやんみたいな感じで、
もう買う買うかみたいな感じのレベルで対応してたんですよ。
強いな。
ただ、書けないものがやっぱりちらほらいくつかあって、
例えば、私はこの時期に定理証明支援系とかっていうのを触り始めていて、
定理証明支援系っていうのは要するに数学の定理とかっていうのを
開発環境と対話しながら書いていくんですね。
ここまでは証明が通ってるっていうラインがあるんですね。
その先にカーソルを進めると、これを証明せよみたいなのが出てきて、
それを人間が証明して、
合ってれば通るし、合ってなければ通らないしみたいな感じの、
だんだんと証明が通ってるみたいな感じの、ちょっと不思議な開発環境があって、
あれですかね、なんかPythonで言う、
ノートブックでしたっけ?
ジュピタノートブックみたいな。
ジュピタノートブックみたいな感じですかね。
ジュピタノートブックあんま使ったことないんでわからないんですけど、
ちょっと違うかなと思いますね。
あれはどっちかというとレプルに近いようなイメージを持っていて、
あれとはちょっと違っていて、
開発環境の下に一個だけ証明状況の窓があって、
今カーソルのこの位置で証明しなきゃいけないものは何かみたいなことのゴールが示されてるんですよね。
そのゴールと今使える前提みたいなのが前の方を見るとわかるんで、
その使える前提からゴールをどうにかしてくっつけるっていうふうなことが人間の仕事になります。
すごい特殊なUIですね。
カーソル位置が状態を持ってるってことですね。
そういうことです。
ここは今何のヒントを出さなきゃいけないかみたいなのを定理証明支援器は知っているって感じなんですよね。
数学の証明っていうのは大体その前提があって、証明したい規決があってっていう感じです。
例えば1たす1は2であるとかっていうのがあったときに、これ前提はなしですね。
規決は1たす1イコール2ってことを証明したいっていうのがあって、
それをいろいろなことを使って証明していくんですよね。
1たす1イコール2っていうのはどう証明するかっていうと、
自分が使っている定理証明支援器のイザベルっていうのだと、
この足し算とか自然数とかっていうのは、ちょっと難しい話だったかな。
ペアの残りっていう方法で作られていて、まず0が1個あります。
0にもう1個交者関数っていうSACっていうのがいて、
1はSAC0です。
2はSACSAC0です。
3はSACSACSAC0です。
っていうふうな感じでやってあげると、
これで自然数を表現できるなっていうのがわかるかなと思います。
変数的な意味。
これはあくまで自然数の1、2、3とかっていうシンボルとか受信数とかでやると大変だから、
あくまで0と交者関数っていう2つの組み合わせで、
自然数の大体全部が表現できるだろうというふうなことを考えた偉い人がいるんですね。
その人の流儀に従って作られていて、
足し算とかイコールとかは全部そういうふうな形で定義されているんですよ。
例えば足し算っていうのは、
どっちでもいいんですけど、
左側が0になるか右側が0になるか、
どっちでもいいんですけど、
左側が0になるまで右から左にSACを移していくみたいなことがありますよ。
何だろう、相当的なものなのか、それともそういう計算式なのか。
そういう計算式なんですよね。
それが自然数の足し算の定義なんです。
だから例えばSAC0SAC0が1SAC1なんですけど、
そうすると今右側にSACがあるんで、
これ左側に移すんですよ。
SACSAC0SAC0になる。
そうするとSAC0は左の数でいいじゃないですか。
だから左の数になってSACSAC0は答え、
つまりSACSAC0は2だったってことなんで、
1SAC1イコール2ってことが証明できたっていう。
なるほど。
だんだんと前提と期決とかっていうのを変形していって、
くっつくところに持っていく。
今の場合は足し算の定義を展開するってことをやったわけですけど、
そういうことをしてあげると、
この証明するしたい1SAC1が2だったっていうことに
つながっていくってことなんですよね。
なるほど。
分かったこととしては、
多分言葉だけだと絶対に伝わらない。
分からないと思いますね。難しいですね。
これ聞いてる人で、
今分からなかった人もいると思うんですけど、
分からないのが普通だと思うので大丈夫だと思う。
これはあれですね、
それ単体だけで説明できる回があっても、
いいぐらいの難しさをすごく感じ取りました。
ラジオで話すのは難しいですね。
SAC0とか言われても何のこっちゃってなりますね。
SACとはみたいな感じになるんで。
計算式が図で示されているとすごい分かりやすそうだなという気は若干しました。
そうですね。いつかそういう風なYouTube配信じゃないですけど、
こんな感じで解いていくんですよみたいなのをやってみたいなと思ってるんですけど。
良さそう。
それがイザベルJエリットの時代。
イザベルという感じでしたね。
その時に私はたくさん定理を証明して、
例えば一番私が証明した中で難しかったなって思うのは、
標識的理論というまた難しい理論があって、
それをちょっと理解したいなと思って、
本の中に証明が一応書いてあるじゃないですか。
日本語とかで書いたわけですけど、
それをイザベルで書くとどうなるんだろう?
ちゃんと書けるんだったら理解できるだろうと思って、
理解できてるってことだろうと思って書き写してたんですけど、
めちゃくちゃ難しかったですね。
表現がどう表現していいかわからないってことですね。
それもありますし、
何なら端折られてる行間の証明が難しいみたいな。
これは地名だろうみたいな感じで書いてるところ。
地名とまで書かれてなかったんですけど、
行間がすごく難しくて、
ここって何が起こったの?みたいなのが結構あるんですよ。
著者の方に直接質問したいみたいな感じになるってことですよね。
実際色々と試していくと、
こういうことだったのかみたいなのは最終的にはわかるんですけど、
なかなかすごい時間がかかるんですね。
ちょっとそれがどれくらい辛い作業かっていうのがわかる話があって、
私は朝の証明みたいな感じで、朝の証明活動みたいなのをしてたんですよ。
朝活みたいな感じで。
7時から8時とか9時くらいまで証明をして、
その後仕事行ってみたいなことをやってたんですけど、
もう10時くらいになってるとヘロヘロになってるんですよ、脳が。
頭使いすぎですって。
もうダメになってて。
それで1ヶ月くらい続いて、ダメだこれは仕事側にならないって気づいて、
朝活動を辞めました。
すごいな。今1ヶ月続けたってことですね。
平日。
あれはちょっとやばかったですね。
仕事の市販機とか、判議ごとに評価があったんですけど、
ちょっとまあやばいなって思ったんで辞めました。
支障出るなって。
支障出るなって感じですよね。
面白い。
そのくらい難しい。
あれですかね。
無理やりプログラミングとかに置き換えると、
OS作るみたいな感じですか?
どうなんだろう。
どっちかっていうと、
アルゴリズムのピタゴラスイッチみたいな感じが近いのかな。
解きたい問題があって、
Aの時は上手くいったんだけど、Bの時は今度は上手くいかなくなって、
Bの時を直したら今度はAの時がこけてみたいな、
モグラ叩きみたいな感じが感覚としてよく似てるかなと思いますね。
こっちから攻めようかなと思って山を登り始めると、
途中で2回木崩れとかがあって、
ダメだこれ。って引き返して、
じゃあこっちかなって思って行くと、
たまたま合ってるみたいな、そんな感じの。
難しい競技プログラミングの問題を解いてるみたいな感じですかね。
そんな感じなんでしょうね。
ただやってることは入門編の教科書なんで、
入門編の教科書でもやっぱり証明って難しいんですねっていうことはよくわかるって感じですね。
数学科の人たちがすごすぎるっていうこと。
これはちょっと私の聞き借りの知識なんですけど、
イザベルとかロックとか、最近だったらリーンとか有名ですよね。
とかっていうのを使う証明っていうのは、
使わないその証明よりも、
ちょっと種類が違うみたいな話を聞くんですよね。
よく私が聞いたことがある話だと、
激しい数学って呼ばれてるような、
そういうのが数学科の人にはわかるらしくて、
そういうのだと定理証明なんて使ってられないと。
多分その教科をかなり読まないといけなくて、
証明がめちゃくちゃ長くなっちゃうからなんでしょうね。
なるほど。
だと私は思ってるんですけど、
そういう分野もあるぐらいで、
そういう分野の証明はもっと難しいでしょうね。
だからもうちょっと範囲が広いっていうか、
もう自明なものはコンポーネントとして
使っちゃおうみたいな話なんですよね。
きっとその数学科の方は。
だけど実際イザベルとかで書くときには、
証明されてる定理はいくつかあるんですけど、
それが自分の使える定理とは限らないし、
なんなら私の場合は、
イザベルの中に入ってる定義と、
私の教科書の定義っていうのがずれていて、
そういうことがあるんですよ。
同じ名前なんだけど定義がちょっと違ってよくありますよね。
例えば高校数学の時の自然数って1からじゃないですか。
だけど大学数学からでは0からだと思うんですよね。
っていう風に定義、
名前同じなのに定義が違うみたいなのがあって、
確かに。
組み込みの定理全く使えなくてっていうことはありましたね。
なるほど。
てか組み込みの定理、
証明済みのものが、
ライブラリーみたいな感じに存在するってことなんですね。
そうそう。
面白い、それは。
それがないとむしろ辛いんですよね。
本当に定義って、
パチッとはまるとすっごくショートカットできるんですよ、
いろんなことを。
なのでそれがいかに充実してるかってことは、
すごく重要なことで、
イザベルとかは結構充実していた方だと思ってますね。
最近だとリーンがすごい勢いで、
他のイザベルとかロックとかを置き去りにするぐらい、
発達してるなって感じがしていて、
将来的にはリーンとかがめちゃくちゃ強くなるんだろうなって感じがしますね。
なんか面白いですね。
完全に話してることは全然違うんだけども、
普通にライブラリー使ってんだろうなっていう感覚と全く一緒なんで。
そう。
でも定理証明試験にも色が結構あって、
リーンだとまた変な流儀に従ってたりとか、
イザベルだとイザベルのまた流儀みたいなのがあって、
それはそれで結構面白いっていう感じなんですよね。
ちなみに全然違う話だなと思って聞きますよ。
最近のOSSってセキュリティのだらで、
依存関係をできる限り少なくしていきたいなというのが個人的な目標であって、
依存しているライブラリーに悪意ある行動が仕込まれたら、
こっちにも影響が来るので、できる限り依存関係少ない方がいいは、
今のところは真理かなと思ってます。
この定理の証明の話でも、証明済みのもの定理が
ライブラリーみたいな感じで存在すると。
それって全然違うと思うんですけど、
セキュリティ的にそれを使っていたらパソコンがやばいとか、
そういうのあったりするんですか?
面白いですね。そんなこと考えてなかったな。
実行系があるのかどうなのか。
まず直感的にはセキュリティ的にやばい構造を実行することはおそらく可能だと思います。
可能なんですね。
なぜかというと、これはごめんなさい。
私も少し半端な知識で話をすることになるんですけど、
証明するときにタクティックと呼ばれる前提をちょっと変化させたり、
起結側をちょっと変化させたりとかするような、
変化させるようなコマンドを作ることができるんですね。
自分で作ることができる。
そのコマンドの正しさ自身はもちろん自分で担保しなきゃいけないんですけど、
このタクティックに悪さを仕込むことはおそらくできるだろうと思ってます。
なるほど。
フックみたいな形で任意のコマンドを実行できるっていうことですね。
例えばISABELLとか、確かSTANDとMLとかでそういうのを書くんですけど、
その中で例えばどんなことをやってるかっていうと、
あるものはSMTソルバーとかSATソルバーとかって呼ばれてるような、
論理式がこれ合ってますかみたいなことを、すごく雑に言うと合ってますかみたいなことを調べてくれるやつがいて、
その調べてくれるやつに丸投げするっていうコマンドがあるんですよ。
つまり証明したいことはよくわからんけど、
なんか反例何だったらええんじゃんみたいな、
なんかすごい雑に言うとそんな感じなんですけど、
とかっていうコマンドを作ることができて、
今それSATソルバーとかSMTソルバーって他のプロセスとかライブラリーとかがリンクして呼び出してるわけで、
要するになんでも好きなことができるってことですよね。
だから証明読み込んだだけで悪させるってことはおそらくできると思います。
なるほど。
次の攻撃対象になっちゃうかもしれないですね。
そこは。
間違いなく開いただけで実行されるためのものではあるので、
その可能性はありますね。
ただこれはちょっと私リーンとかはあんまり使ってないんでわかんないんですけど、
イサベルに関してはそのタクティック仕込むの結構大変なんですよ。
なんかちょっといろいろとカウント編成とか追加したりとかいろんな面倒くさいことしなきゃいけないんで、
なんかあんま簡単ではないとは思ってます。
サクッと入れられるものではないからこそ、
そこに関しては防御ができて、
実行時の防御はできてないけども、
環境を整えるというような防御ができている。
気軽にはあんまりそういうふうなマルウェアは入らないって感じですね。
あと攻撃者としても、そこを叩いたとしても、
そういうのを使っている人たちの環境をダッシュしても、
そこまでいいことないかもなみたいな、
そういうのはありそうですよね。
実際隔離環境に置くことはすごく簡単で、
外部通信とかしないですかね、定理証明って。
するものもあるんですけど。
あるんです。
リモートヴァンパイアってやつがいて、
ヴァンパイアっていうのが定理証明神経のソルバーの一つで、
自動で証明やってくれる君みたいなやつなんですよ。
リモートヴァンパイアっていうのは、
サーバーにそいつがいて、
そいつがこれ証明してよって投げると、
ぼくぼくぼくって回ってくることがあるみたいな。
サンズじゃん。
そういうのもいるっちゃいる。
ただそれはローカルのヴァンパイアを動かせばいい話なんで、
ローカルでヴァンパイアを動かしてってことをやれば、
リモートとの通信は一切なくなるんで、
サンドボックスはすごく簡単に成立するって感じですね。
そうですよね。
だからそういうわけわかんないプロセスぶったたくものに関しては、
全部サンドボックス上で、
隔離環境で実行してしまえば何も問題はないですもんね。
簡単な話どっかコンテナ立てて、
そこの中でやればいいわけだし。
それで全く問題ないって感じですね。
そうですよね。
環境としてもかなり独立したものだと思うんでね。
他のものを入れたいとかそういうのもあんまりなさそうなんで、
それでいいっていうような話を、
かなりこの照明の部分だけで話しちゃったんですけど、
次の開発。
次の時代が、その次にAI時代が来たんですよ。
クロードコードとかコーデックスとかジミーとか、
いろいろなものを使ってみたんですけど、
結局私はクロードコードに戻ってきましたね。
いくつか好きでコーデックス使ってたんですけど、
いくつか意に沿わない行動をされたことがあり、
なんかちょっと違うなっていうので、
そういう体験がすごく少なかったクロードコードに最終的には戻ってきちゃいましたね。
ちなみにアンチグラビティ、今だったらアンチグラビティCLIかな、
ジミーの場合は。
もう使ってみたりとかしたんですか?
使ってみました。アンチグラビティはもうちょっとひどかったなっていうのが結構あって、
ひどかったね。
使ってよかったなっていうシーンがいくつかあって、
ジミーのいいところはAPIが安いっていうのが一つ。
安いですね、Googleは。
そうともう一つは命令追従性が高いっていうのがあって、
なんかやれって言ったらはいってやってくれるみたいなイメージがあって。
従順な。
クロードとかコーデックスは余計な手を利かせてくれるんですよね。
確かに。
余計な親切をやってきちゃうってところがあって、
ジミーはそういうの一切しないでやれって言ったことだけやってくるんで、
それはそれで助かるシーンがあります。
例えば文章を書くときとかにアウトラインを作って、
私はよくアウトラインをマインドマップで書いて、
それを深さ優先探索すると記事になってるみたいな感じの書き方をするんですけど、
そのマインドマップから原稿のその損は起こしてくださいっていうと、
クロードコードとかコーデックスにはすぐこうなんか冗長な、
いらないもの、余計なものを付け足しちゃうんですよ。
なんだけど、ジミーには本当にそこから素直に読みやすい、
さらっと読める文章に返ってきたんで、
これはちょっといろいろと、
最近AIの冗長さを減らすようなスキルとかってあるじゃないですか、
ヒューマライザーとか、あとはジャパニーズテックライティングっていうのを
シカノさんが出してましたよね。
っていうのを使ってみた結果、一番良かったのが
ジャパニーズテックライティングとジミーの組み合わせ。
全部自分が生成させて、人間でブラインド評価させてみたんですけど、
やっぱり一番良かったのはジミーにプラスチックライティングだった。
一番冗長さが少ないって感じなんですよね。
ジミーにも使い道が良ければあるっていう感じだと思いますね。
コーディングじゃなくて、かつAPI呼び出しで、
API安いし、フラッシュとかライトとかだったら安いし、
そういったところで使っていくみたいなのがジミーの方向性。
自分自身もそんな方向性で使ってるんで、
かなり同意だなというところなんですけど、
でもコード自体はクロードコードを使ってやってる。
そうなんですよ。これはちょっと不思議だなと思ってるんですけど、
私はかなりはっきりといろんな命令をするタイプなんですね。
命令しなかったことで自由にやっていいって考えているタイプなので、
そういう人ってどっちかというとコーデックスの方が向いてるってよく聞くんですよ。
コーデックスの方が尺手定義なんで、
向いてるってよく聞くんですけど、
コーデックスが余計なことを立派にしてくるっていうことを何回か経験していて、
例えば城寨繊維図の中に論理式が書いてあるんだけど、
論理式は英語に直されたことがあるんですよ一度。
直せとは一言も言ってなくて、
ここにこの辺足してって言ったら全部英語に直されて、
これ何言語ですかって言ったら英語ですって言われちゃって、
いやそういうことではないみたいな感じのことがあって、
それでコーデックス使うのやめちゃったんですよね。
そう、しれっとそういうことをしてくるんで。
ただ、レビューとかはコーデックスの方が優れてるって人はよく見かけますね。
ちなみに今その両方を使ってるってわけではないってことですか?
今私が使ってるのはクロードコードとほぼGeminiのAPIを使ってるみたいなそんな感じです。
組み合わせ、使うとこでGemini使ってってことですね。
なのでコーデックスはあんま使わなくなっちゃいましたね。
人によってはレビューだけコーデックスにやらせたりとかってことをしていますけど、
私はそれもやめちゃったから、クロードコードのエージェントモード、サブエージェントでレビューさせるだけで
結構十分なレベルに達してきていると判断しましたね。
使い方ですよね。何回かこのPodcastでも話してきてますけど、
クロードコードの指示出しみたいなところで絶対にテストを書かせるだとか、
そういうワークフローが今だったら現状だったらクロードコードが一番適してそうだなっていう。
そうですね。あとはやっぱり前回だったっけな、話をしたここの部分念入りにチェックして
フォーカスさせるって入れてあげるだけで、多分コーデックスに変えてあげるっていうよりかは
フォーカスさせてあげる方が私は効果が高いっていうのが体感で、
なのでそれで十分サブエージェントプラスフォーカスさせてあげる機構意識って
私はもうコードをほぼレビューしなくなりましたね。
だからもうモデルじゃない説。
そうモデルじゃない説ですね多分。ワークフローとかそっちに近いですね。
ワークフローとか今だったらハーネスっていうのかもしれないですけど、
そういう外の部分ですよね。使い方だって。
使い方じゃないかもしれないですけど、何か使わせ方?
みたいなところなんですかね。重要なのは。
もう何かモデルの性能もさちってきてるというか、何かもういいんじゃない?みたいな感じになってきてる。
私もちょっと分かんないんですよね。フェーブル使っててすげーすげーって言ってる人たち確かにいるんですけど
私はもう全然オーパスで十分だなと思ってて、オーパスずっと使ってます。
自分も全く同じ意見ですね。
フェーブル5ですごいって言われてるけども、そうだよねっていうような感じになっちゃってるんで。
何なら時々ソネット使ってるぐらいで。
俳句は使ったことあんまないな。動作確認するときに俳句使いますね。
mcpこれ読んでる?って質問するときにその俳句とか使いますね。
軽くね。
だから重要なのはもしかすると、どのモデルを使うかというよりかオーケストレーションの方かなって思ってきてるんですけど。
どうなんでしょうね。ただやっぱりソネットの方が変なことをしてくるっていう印象はやっぱりあって。
確率論でね。
だからモデルは大事なんだと思うんですけど、ただもう十分な数字に達してきているオーパスでっていう気はしていますね。
いやそんな気がします。なんかもうすでに人間の能力を超えてるから。
そうそう。
人間の能力を超えてるっていうのはちょっと語弊があるなと思ってて。
人間って能力って山みたいなもんだと思っていて。
例えば私かなんかだとテストとかのほうには山の頂きの部分がある。
例えばDBとかのほうは瀬須野もいいところ、谷みたいなところにあるんですよね。
そういうふうに人って得意不得意があるじゃないですか。
その得意不得意の得意の山はまだAIに超えられてないというふうな感じはするんですけど。
AIって万能選手じゃないですか。どれもこれも平均より上のレベルで来るって考えると。
全部80点ぐらい取ってるみたいな。
80点70点ぐらいで来るんで、全部が全部70点80点の人間なんていないでしょって思うんですよ。
スーパーマン。
スーパーマンですよね。だからまだ人間の最高峰の部分はまだ残っているとは思ってるんですけど、
ただやっぱりとにかく全部が70点80点っていう選手は驚異的な姿勢だと思っていて。
そういうふうな捉え方をしていますね。
確かにその通りかもしれないですね。これで多分言えることって人間どこで生き残っていく仮説あるじゃないですか。
エンジニア度数の問題。1個で突き抜けろって話ですよね。今の話。
そうですね。1個で突き抜けろ。ただ難しいですよね。
最近AIが証明をバンバン数学の難問から解いていってるじゃないですか。
私も解説を読んだだけなんでそんなに詳しいことがわかっているわけじゃないんですけど、やっぱり異分野との融合みたいなところが強かったらしくて。
この分野の難問なんだけどこの分野の知識を使うと解けるみたいなところがあって、ここに接続するのかみたいなことの驚きがあったって数学者が言っていて。
そういう話を聞いているとやっぱりさっきの全部が全部70点だと見つかる問いがあるっていう話なんだと思っていて。
昔よくそういうこと言いましたよね。よく人間って一本で一本槍やめろと。
2本槍持って重ね掛けしてニッチな世界にすればそのニッチな世界でてっぺんを取れるという言い方をしたと思うんですけど。
パイ型人間みたいなことかな。
だけどそれはだいぶ戦略としてAIにやられたなって感じはしていて。
そうわかります。
どうしたらいいんでしょうねっていうのは正直わからないですね。一本足の方がいいのかもしれないしどうなんだろう。正直読めない。
多分あれかなと思っているのが国明さんの場合はテストが大好き、照明とかが大好き。大好きを極めるんですよ。
それはそうかもしれないですね。
偏愛を極めるみたいな。そういうことなんじゃないかなと思って。
AIって大好きとかないと思うんで。それを極めていった先がニッチになっているっていう。
それでポジションを取ってるみたいなところが人間が残されるべきところなんじゃないかなと。
あとやっぱり私がAIに圧倒的に人間に勝ってるなって思うのはエネルギー効率ですね。
景気1個で照明の結構いいところまで溶けたりするわけですよ。
でも朝かつで疲弊するけど。
朝かつで疲弊するけど。そうだけど疲弊するっていうのは川とかを日上がらせるほどのエネルギーを使うっていうわけじゃないんですからね。
確かに水いっぱい使うわけじゃないですよね。
そう全然使う。何ならさっき言った通りドーナツ1個とかコーヒー1杯とかで動いちゃうわけですよそれが。
それは驚異的だと思うんですよね人間のエネルギー効率って。
だから今のAIのエネルギーとかっていうの収支を考えた時に本当にちゃんと黒字なんだろうかって思うわけですよ。
エネルギー収支とかに。値上がりつけるんじゃないかなって気はしていて。
フェーブルとか使うのにめっちゃ金かかんないと無理みたいな。
そうなるとまた人間の世界が若干戻ってくるなって気がするんですよね。
安いモデルをいかに効率よく使うかみたいな。そういう勝負になってくるってこと。
そうですね。人間は安く早くそしてコンテキストが長いっていう計算機であって、AIはコンテキストが小さい、広く薄く知っているみたいな。そんな感じの使い分けになるのかなって気がしますね。
AIに任せると高いから人間を使うという地下労働施設が存在するということですね。
そうですね。ちょっと人間を無視した発言をしましたけど。でも純粋にいろんな物事を計算機とか問題を解く何かというようなこととして捉えると、やっぱりエネルギー効率ってすごく大事だなって思っていて。
今のAIを使っているやつとかやっぱり無理しているなって気がするんですよね。環境に対してとか電力に対してとか。
そのあたりとかっていうのがちゃんと安定した世界、収支がちゃんと取れている世界になった時にAIは一体いくらするんだろうって思うんですよね。今は無料バーゲン中みたいなもんだと思っていて。
今はバブルなので。
そうですよね。
なんか投資が投資で膨らんでいってどんどん投資をしていくみたいな。で、どこかで机が払わされてはじけるみたいな。そんな時代だと思うんですよ。
だからそうなった時にだいぶ、我々は黒と黒とか取り上げられちゃうわけですけど。
それはそれで辛いわけですけど。
どうしようってなる。
そういう世界が来るのかなって気がしてますね。ただ読めないですね。
読めない。
例えば人間が今のAIみたいな思考を低電力でできる、低エネルギーでできるってことは理論的にはそれぐらい近づけていくことはできるだけなんですよね。バイオコンピューターとかに落としていけば。
今のシリコンでやってるコンピューターだからそういうことがエネルギーとかちょっと消費しちゃうっていう話なわけで。
そう考えると本当にどうなっていくんだろう、技術の方向性がどうなっていくとか全く想像つかないですね。
例えばデータセンターを宇宙に上げるみたいな話もあるし。
どういうふうにこのAIが作った問題を人類は解決するのかってのは読めないですね本当に。
わかんないですね。ちょっと開発環境の話から若干話が…
それできたんですけど、クロードコードを今は大絶賛使っている機っていうようですね。
ちなみにクロードコードを使っていて、多分CLIから使っているのかなと思うんですけど、Vimとかって逆に回り回ってまた使い始めてみたいな話がありますよね。
ありますあります。クロードコードとかって普通のプロンプトを入れるところって回復できないじゃないですか。回復できないってことはマークダウンとかかけないんですよ。
シフトを頑張って押して会議をしたりとか。長文書きづらいですね。
実はプロンプトでコントロールGって押すとVim開くんですよ。多分エディター環境変数のエディターが開くんだと思うんですけど。
そうすると好き放題Vimで書いて保存して閉じるとそれがちゃんとプロンプトに入っているみたいな感じのことができて便利なんですよね。
それは私結構頻繁に使ってますね。
Vimを立ち上げる頻度は逆に上がっている?
上がりましたね。だいぶそれのためにプラグイン減らしましたね。読ませるプラグインを。
起動速度を上げるために。
確かにそこが影響してしまう。クロードコードからプロンプトを書くためにVimを毎回ロードしないといけない。逆に数で使ってないですね。
ちょっとだけ入っちゃってるんですよ。特にこれ離れられてないのがサラウンドっていうのがあってカッコをいい感じにしてくれるプラグインがあるんですよ。
ティムポープって人が作ったやつがあるんですけど。
閉じカッコ?
閉じカッコを言ってるのは別のやつですね。どっちかというと今選択している領域の外側にカッコをつけたりとか。そういうことができるんですよ。
そういうのとかにサラウンドっていうのを使っててそれがちょっと離れられない。
なるほど。
自然言語を書くのにも必要だから。
必要になっちゃうんですよ。カッコってどうしても今選択しているところをカッコ行きにしたりとか結構あって。
やっちゃうんですよね。でもだいぶコードの補完用のものっていうのはいらなくなってきていて。
閉じカッコのさっきの話出てきたんですけど、閉じカッコって実はVimとかだと素朴に実装するといろいろやばい挙動を踏むんで、ちゃんとしたプラグに使いなさいってよく言われてるんですよね。
Neximaとかそういうところを使おうっていう話をよく聞くんですけど、恥ずかしながら私は使ってなかったんですけど、それから全部消しちゃいましたね。
もう別に閉じカッコで釣り合ってるみたいな感じのことをVimで書くことが減ってしまったっていう。
あとあれですよね、単一ファイルの編集になると思うので、単一ファイルじゃないですけど単一メモリの編集になると思うので、ファイル釣りとか絶対いらないですよね。
あとだ、一括でのリネームとかあるじゃないですか、あれってすごく面倒くさいと思ったことありません?
例えば連番のパディングの数字が001だったのを00001みたいに増やしたいみたいなときあるじゃないですか。
そういうときにリネームするのってすげえ面倒くさいじゃないですか。シェルスクリプトとか組まなきゃいけなくなっちゃう。
ちょっと面倒くさい。
あれ私Vimのプラグインでやってて。
なるほど、そういうので。
あれはめちゃくちゃ使いやすいですね。
シェルで書くんじゃなくてVimのプラグイン経由で。
Vimで編集してやってるんですけど、むしろ私はファイラーが手放せない。
すげえニッチな使い方してる。
多分僕が今やろうと思ったらクロードコードにお願いしますよ。
なるほど。
フェーブルさんにお願いします。
なるほど。
そのためだけに。
これは電力の無駄遣いなんでやめた方がいいと思うんですけど。確実に。
ファイラーとそのさっき言ったサラウンドは手放せなくて。
ラッドはいくつかマークダウン開くときにスノーのやつだとちょっとマークダウンが遅かったんだっけな。
YAMLか。YAMLですね。
YAMLのスノービームプラグイン、デフォルトで組み込めてるやつはちょっと重い。動作がもっさりするっていう問題があって。
それは別のYAMLのプラグイン使ってるとか。
でもそんな感じのものがちらほらってあるくらいで、機動速度に影響を与えるようなものを入れてないって感じですね。
じゃあもうできる限り少なくして、機動速度速くして。なんだけどもビームRCに書かれてるものはまたちょっとあるっていう。
そうですね。ちょっとどころかまだまだある。
いっぱいある。
会社のほうのと今使ってるドットファイル図って共用ができなくて、今の会社のって個人のアカウントでのログインは禁止されてるので、
ダブルのアカウントが分かれちゃってるんですよ。
ちょっとめんどくさい。
会社のほうはちゃんとそのビームのプラグインをビームプラグとかに移したんですけど、
今普段のプライベートのほうは全然移せれてなくてとかっていう問題があります。
だから私のドットファイル図見ると、あいつあんなこと言ってたのにまだネオワンドル使ってんじゃねえかみたいなことになると思うんですけど、それはそういう理由です。
まあちょっとしょうがないっていう。
しょうがないって感じですね。あんまりプライベートで開発することがだいぶ減っちゃったんで、そうなっちゃってますね。
じゃあやっぱ回り回って逆にビーム使い始めてますね。
そうですね。ビーム使い始めましたね。
やっぱり本物のビーム使っているときが一番いいですね。
やっぱりJetBrainsのビーム使ってたときって痒いところがいっぱいあるんですよ。
ここのときのこの挙動が普通のビームと違うみたいなところがめっちゃあって。
あれってただのキーバインドがビームになっている、ビームっぽいよねっていうような拡張ですよね。
そうですそうです。ただビームってモードがあるじゃないですか。今インサートモードです、今ノーマルモードですみたいな。
ビジュアルモード。
ビジュアルモードとかいろんなモードがあって、あのモードを作るのって大変だと思うんですよ。だって元々はないんですよ、モードなんて概念は。
いやめちゃくちゃ大変。
だからそのモードとか、ただのキーバインドだけだったら簡単なんだけど、そのモードとか含めたいろんなものをやっているのってすごく涙ぐましい努力がいくつか見られてて。
例えばVSモードとかのビームのノーマルモードとかの下のコマンドモードとかするときに、下のステータスパー文字しか書けないのにそこで頑張って表現してるんですよ。
カーソルなんてあるパイプですよ、バーティカルが使ってて。それでその文字カーソルを表現してるみたいな感じになってて、涙ぐましいなって思うわけですよ。
だからもう再実装してるってことですね。
そうそうそうそう。
あのエディターのプラグイン上で。
ほぼ同じようなことを。
そうなんですよね。だからそのあたりはすごい、なんかたかがキーバインドとは言えないなって思うぐらい苦労してるなって思います。
それは確かに、それはなんかビムを好んで使ってる人のなんでしょうね、執念というか。
そうですね。
印象に残ってるのが、いつだかのビムコンフっていうそのカンファレンスがあって、いつだかのビムコンフでAtomってエディターあったじゃないですか。
今は無き。
今はもうあるのかな、ないのかわかんないですけど。
いやない、もうクローズしちゃいましたね、Atomが。
Atomにそのビムプラグイン作ってた方がいて、それがすごくこう、いろいろそのビムの考え方とかっていうのを整理し直していい感じで実装した方がいて、それはすごくすごいなって思いましたね。
やっぱり後発だからこそ概念を整理して、要するにリファクトされた状態でリリースできるっていうのはいいことだなって思って。
いい点ですね。
今聞くとそれネオビムなんじゃないのって思っちゃう。
ネオビムはまた全然違う理由で報告されてると思うんで、わかんないですけど。
またちょっと違う。
ネオビムもちょっと使ってみたいですよね、私はスノビムの方をずっと使ってるんで。
ビムがすごく大好きな人はネオビムじゃなくてスノビムを使い続けるんだろうなというなんとなくの印象が。
単に過去の資産から逃れられないというだけの気がしてる。
そういうこと。
そうそうそう。
ただ私もだいぶプラギン減らしちゃったんで、今だったらネオビムでも生活できるかもしれませんね。
速度の面とかもあるかもしれないな。
速度の面の話は確かにそうですね、ネオビムの方が早いんだろうな。
ビムもそのビムナインスクリプトっていうのがあって、コンパイル言語みたいなものが入るんだか入ったんだかちょっとちゃんとは覚えてないですけど、っていうのがあって。
それが入るとだいぶ速くなる。
だいぶ速くなるって言ってもビムスクリプトってめちゃくちゃ遅い言語なんで。
どこなんでしょうね。
どこまでなんだろうなっていう。
そうそうそうそう。
どこまでなんだろうなっていう感じですけど。
私がビムスクリプトの静的解析機を書いた時にビムスクリプトで書かなかった理由はビムスクリプトがめちゃくちゃ遅いからなんですよ。
ただでさえ遅いって言われてるPythonよりもめちゃくちゃ遅いぐらいなんで。
話にならないぐらい遅いんで。
それで、やっぱりNeoビムとかに勝手ない部分があるのかなって思うんですけど、ただなんだろうな。難しいですね。
Neoビムと今のビムってなんなんでしょうね。
Neoビムの方がすごい活発だろうなって思ってるんですけど、私は活発よりかは枯れてる方を好むので。
っていうのもあって私はビムを使ってるのかな。
なるほど。ビムの方が歴史もあるしっていうところですね。
そうですね。やっぱり枯れてるとメンタルモデル変えなくていいんで、アップデートしたら壊れたみたいなの繰り返さなくてもいいですよね。
それはでかいですね。
現状で満足してるんですよ、ビムで。
逆にクロードコードのおかげでCLIに戻ってきてビムを使い始めたっていうのはやっぱり面白いなと思いつつも。
ビムの次に使ってたジェットブレインズ製のエディターを使わなくなってきたっていうのがマジででかいなと思ってて、僕自身。
僕もジェットブレインズずっとアルティメイトかな、ずっと使ってて、全てをそれで賄ってたんですけど、ある時期以降カーソルに移動して全てを使わなくなってきたっていう経緯があるんで。
ジェットブレインズさんありがとうございましたというような感じなんですけど。
ジェットブレインズやばいと思いますね。どうなっちゃうんだろう。
すごく私はジェットブレインズ製品好きでTシャツとか持ってるくらい好きだったんですけど。
好き、マジで。
でも今使ってない。
商業無常ですよね。
難しい、本当に。
でもまたこれでジェットブレインズが盛り返して次のエディターになってくる可能性もあるんでね、またビムに戻ったような。
ジェットブレインズAIってあるじゃないですか、あれどうなんだろうって話をあんまり聞いたことがなくて、使ってる人が周りに全然いないんですよ。
厳しいと思いますよ。
そうなんだ。
いろいろジェットブレインズ製品AIが出る前から、例えばGitHubの開発環境をオンラインで使えるようになるみたいな。
クラウドで開発環境を用意してそこに対してエディターをアタッチできるみたいな。
っていうのが同じようなものがジェットブレインズにもあって、それ使ったんですけど、やっぱGitHubとかの方が性能がいいんですよ。
そういう形で、ジェットブレインズって僕の印象ですけど、ローカルでのエディター、しかも言語特性を理解したエディターにかなり特化してるんですよね。
それ以外が弱いっていう印象で。
そうかもしれないですね。
厳しいなっていうような。
厳しいですね。
戦いとしては。
しかもジェットブレインズ邪魔ベースですよね、全部あれ。
邪魔です。
例えばもう少し邪魔スクリプトに近い言語だったら、まだウェブプラザとかに移植が簡単だと思うんですけど、邪魔。邪魔か。
その領域は完全にもうアトムの次になったVSコードですね。
VSコードがもうすでに取ってるので。
派遣取っちゃいましたからね。
私もイザベルはJリットだった時代からVSコードに乗り換えたんで、良かったですね。
それはすごく感謝してるんですけど、ただVSコードいまいちなぜあれが派遣を取れたのかよく分かっていないですね。
なんでなんでしょうね。
ビジュアルスタジオっていう名前がついてるから。
でもなんかVSコードの左側のペインとかっていうのは正直分かりやすい感じがしないんですよね、あんまり。
分かんないですね、分かんないです。
いっぱい増えるし、よく分かんないです。
あんなにみんなモテ生やしてるんだろうっていうのは正直よく分かんない。
リム使ってる奴が何言ってるんだって話はあるんですよ、もっと分かりにくいものを使ってる人が。
それはそう。
そうなんだけど、別に言うほど初心者向けって感じでもないし、なんでVSコードが勝っちゃったんだろうなって本当に不思議ですね。
そこしかなかった可能性はあります。もしかすると空白地帯で収まったみたいな、そういったことはあるかもしれないですけど。
でも前世はCLI時代だと思う、TUI時代だと思うので、若干VSコードから離れてるかなと思いつつと。
今回結構開発環境というか、開発環境から始まっていろんな。
単純にいろんなところ聞けたかなとは思いつつ。