10年前から文章の理解しやすさの認識がだいぶ変わった。昔は論理式やそれに相当する固い説明がどっさり書かれている文章を理解しやすいとは思わなかったが、今ではコンテキストさえ掴んでいれば論理式やそれに相当する固い説明で書かれた文章の方が理解しやすいと感じる。たとえば論理式やそれに相当する固い説明がどっさり（本当にどっさり）書いてあるソフトウェア科学基礎や型システム入門を理解しやすいと今は思う。たとえば、ソフトウェア科学基礎には以下の記述がある：

s が無限回含まれるとは，任意のi ≥0 について，s = s j となるあるj ≥ i が存在することである．

── ソフトウェア科学基礎 p.198

昔だったら、この記述を理解しやすいとはきっと思わなかっただろう。「s が無限回含まれる」なんて論理式の説明がなくともわかるし固い説明なんてしなくていいのではと思っていははずだ。しかし今ではこの記述を理解しやすいと感じ、さらにこのような記述はあるべきだとまで思っている。

この認識の変化はなぜ起きたのだろうか。振り返ると、数学基礎論の初歩を理解したことが鍵だったように思う。

数学基礎論の初歩を理解すると、論理式の意味の理解や、形式的な証明をできるようになる。私はここに とてつもない価値 を感じている。しかし世間を見渡してみればこの要因の価値がわかる人とわからない人の真っ二つに分かれるのではないか。そこで価値がわからない人向けに説明を試みる。この価値のわからない人は「論理式の意味がわからなくとも、形式的な証明ができなくとも、何か物事を理解することはできる」と考えていると思う。そこで思考実験をしてみよう。ある難しい理論を易しく説明すると謳う文献が理論の当てはまる例を1つ2つだけ紹介している。この文献を読めばその理論を精密に理解できるだろうか？私は例をいくつか知っているだけでは深い理解にはならないと思う。深い理解とはその理論の対象について多くの主張の帰結を短時間に回答できることだと考えているからである。この定義の上で考えると、例を2つ3つ紹介するような易しい文献を読むだけでは多くの主張の帰結を回答できるようにはならない。ただ短時間のうちに紹介されている例については主張の帰結を回答できるようになる効果はあると言えるだろう。ただ、具体例はわかりやすいがそれだけの説明だと他にどんな例があるかの推測を正確はできない。一方、論理式やそれに相当する固い説明で書かれた文書は親切にも例が書かれていない限り短時間に主張の帰結を回答できるようにはならない。しかし、ひとたび時間をかければ急激に帰結を回答できる主張が増加していき、易しい文献の理解度をいつか追い越す。これを図にすると次のようになる：

この差は思考実験のしやすさに由来している。論理式やそれに相当する固い説明は具体的な対象を割り当ててその真偽を厳密に判断できるため、読者側で実験しすぐに結果が得られる。しかし例を2つ3つ紹介されただけでは、正確に他の例を思いつくことには手間がかかる。似ている例を直感的に挙げることはできるだろうが、それが本当に説明されている理論に当てはまるのかどうかの検証に時間がかかるからである。余談であるが、よく練られた文献は論理式や固い説明を書きつつ例を添えることでそれぞれのいいとこどりをしている（代わりに文量が増えるため鈍器と化す）。このことを一般化すると、個別の例の説明は素早く理解度を上げられるが深い理解には至れず、膨大な例を端的に記述できる説明は深い理解に至れるが抽象的なため理解に時間を要するということだろう。そして深い理解に至るためには抽象的な説明を精密に記述できる言語が必要なのである。そしてそのような言語として論理式が知られている。だから論理式の意味を知ることが何かを深く理解する上で鍵になってくるのである。

ただ論理式を知るだけでは片手落ちである。論理式の意味がわかるだけでは思考実験をしにくいからである。論理式は、決まった手順で論証することで前提が正しければ帰結もまた正しいと言える性質を備えている¹。ここでこのような論証のことを 形式的証明 という。数学の証明もそれが正しければ形式的に証明できる²。ただし義務教育で習う数学のほとんどの証明は非形式的な証明であることから形式的な証明に馴染みのある人は多くない。形式的な証明の最大のメリットは機械による支援が受けられることである。定理証明支援系という形式的な証明を支援するツールがある。Isabelle や Rocq、Lean などさまざまなものが知られている。これらを使うと、主張が形式的な論証に沿っているかの確認だけでなく、主張の自動証明や反例探索ができる。これによって、論理式を使って機械に支援されて主張を実験できるのである。

もうひとつ、言語化できないものを人は理解できないという点も指摘しておきたい。思考は言語に制約されることを痛感したできごとを2つ紹介しておく。

10年前の私にはさっぱり証明の思いつかなかった Promise.all と race の組み合わせによる待ち合わせの表現力の証明を、その5年後にできるようになった。私が10年前に証明を思いつかなかった理由はあり得るケースを網羅的に表現する言語を知らなかったからである。その5年後には操作的意味論をかじり、また状態遷移モデルを扱えるようになったため、前者なら「どのように評価されても」、後者なら「どんな遷移経路でも」と表現できることを知っていた。この知っている言語の差が 10 年前の私に証明できなかった主張をその 5 年後には（否定的に）証明できるようになったという違いを生んだ。

また 10 年前の私はGUIアプリケーションの仕様とは何かを言語化することができなかった。10年経った今では画面仕様書への静的検査器を開発できるほど、GUIアプリケーションの仕様とは何かを説明できる。10年前と今の違いは2つある。1つは仕様とは何かという理解の深さの違い、もう1つは膨大な遷移経路のあるモデルを端的に表現するために知っている語彙の多さの違いである。10年前の私は仕様が何かをはっきりと説明することはできず、これまで読んできた「仕様書」と呼ばれるものの共通項を挙げるぐらいしかできなかった。今の私は仕様がどんな実装についてもその正誤を機械的に判定する基準であると知っている。また、GUI アプリケーションは画面を行って戻ってをいくらでも繰り返せることが多く、その遷移経路の数は無限大であることが多い。すると仕様で許容したい遷移経路の集合や、実装で生じる遷移経路の集合を現実的な記述量で表現する言語が必要になる。10年前の私はそれを知らなかった。10年経った今の私は時相論理や CSP による表現を知っている。そのため、与えられた実装が仕様を満たすかどうか機械的に判断する基準を端的に記述できる。

前者も後者も、言語を知ることでできなかったことができることに変わっている。言語がこんなにも私のできることを広げてくれたのである。それにともなって理解しやすさの感覚が変わったのだろう。