ご来店ありがとうございます。新刊発売予定のお知らせです。
2025年9月4日（木）、井上亜星著 『ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発』の発売を予定しています。
書名にもある通り、本書はLeanという比較的新しいプログラミング言語の入門書です。プログラミング言語としてのLeanは、いわゆる関数型言語の仲間と言えます。 他の関数型言語、とくにHaskellを使ったことがあれば、典型的なアルゴリズムやデータ構造を扱うLeanのコードをなんとなく書けるかもしれません。その程度には「ふつうの言語」であるとも言えます。
しかしLeanには「ふつうの言語」にはない大きな特長もあります。具体的には、「数学の証明をソフトウェアとして形式化できる」あるいは「プログラムの挙動に対する証明ができる」という、定理証明系としての側面です。本書では、そのうち「数学の証明をソフトウェアとして形式化できる」という側面にフォーカスして、Leanによるプログラミングを解説しています。例として扱う数学の題材は、自然数と整数についての性質です。
というわけで本書は、数学の証明をソフトウェアとして扱えるようになりたい方々にとって、「これ一冊で目的地が見えるところまで到達できる」ような本です。おすすめ。
加えて本書は、プログラミング言語の理論にちょっと興味があるソフトウェアエンジニア、とくに「カリー・ハワード同型対応や依存型といったキーワードが気になるけれど教科書を読んでも何が嬉しいのかよくわからない」と感じている方々にとっても価値ある一冊でしょう。Leanで数学の証明をソフトウェアとして扱えるのは、カリー・ハワード同型対応による証明とプログラムの同一視がLeanでうまく実装されているからです。本書では、そうした背景知識についても丁寧に押さえられているので、これまでキーワードとしてしか知らなかった抽象的な概念が現実のコンピューター上で動くプログラミング言語として実体験できます。
「いま数学と計算機の両方に興味がある人はLeanというプログラミング言語が気になっているに違いない」くらいの気持ちで発行する新刊『ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発』により一人でも多くの方にLeanの面白さを知っていただけるとうれしいです！（購入可能になるのは9月4日です）