プログラミングと数学をつなぐ

• 井上亜星 著
• 228ページ
• A5判
• ISBN：978-4-908686-21-4
• 2025年9月4日 第1版第1刷
• 正誤など

ソフトウェアとして数学を扱いたい人、そして数学の力をソフトウェアに結びつけたい人にとってのプログラミング言語、Lean。本書では、動作するプログラムとして自然数と整数を構築することで、数学とソフトウェアがLeanによってどう結び付けられるかを確かめながら、Leanによりソフトウェアを開発するための基礎を身に付けます。

数学の形式化に興味がある数学者はもちろん、数学に挑戦したいプログラマーや、計算機科学の抽象概念を手触りで確かめたいエンジニアにも最適な一冊です。

本書は『n月刊ラムダノートVol.5, No.1（2025）』に掲載された記事「自然数を作って学ぶLean言語」を基に内容を加筆して書籍として刊行したものです。

型システムがようやくわかった！

• 遠藤侑介 著
• 184ページ
• A5判
• ISBN：978-4-908686-20-7
• 2025年4月15日 第1版第1刷
• 本書の解説で利用しているコード（GitHubリポジトリ）
• 正誤など

現代の開発環境では、エディタ上でコードを書いている最中から、実行もせずにエラーが判明することがあります。コードの補完でも、文脈に適した候補が魔法のように提示されてきます。こうした機能で中心的な役割を果たすのが「型システム」です。

では、なぜ型システムはプログラムのエラーを早期に発見したり、適切な補完候補を絞り出せたりするのでしょうか？　背景となる数学の理論を教科書で学ぶ以外に、型システムで何ができるのか、どのように機能するかを知る道はないのでしょうか？

本書では、TypeScriptのサブ言語に対する型検査器を実装しながら、実用的なプログラミング言語の機能が型システムでどう実現できるかを見ていきます。AST（抽象構文木）や処理系の実装を通してプログラミングへの理解を深めるように、型検査器の実装を通して「型システムのしくみ」を覗いてみましょう！

本書は『n月刊ラムダノートVol.4, No.3（2024）』に掲載された記事「TypeScriptではじめる型システム」を基に内容を加筆して書籍として刊行したものです。

TLSとPKIの実像を理解し、サーバとアプリを安全にする

• Ivan Ristić 著、齋藤孝道 監訳
• 488ページ
• B5判
• ISBN：978-4-908686-19-1
• 電子書籍の形式：PDF
• 2023年12月4日 第2版第1刷 発行

現代生活を支えるインターネットでは暗号化が不可欠です。しかし実際にサーバやアプリで通信の暗号化を適切に利用するには、暗号化アルゴリズムの知識だけでなく、セキュリティプロトコルであるTLSとそのWebでの応用、さらには基盤となる信頼モデルであるPKIについての幅広い知識と経験が必要になります。

本書は、TLSとPKIの全体像を体系的かつ具体的に語った‟Bulletproof TLS and PKI 2nd Edition”（Ivan Ristić 著）の全訳です。Webセキュリティが現在の姿へと至った背景を理解し、サーバやアプリを安全にするために自分たちが何をすべきかを知るための決定版。

本書の主なトピック

• インターネット標準のセキュリティプロトコルであるTLS（Transport Layer Security）の基礎知識
• TLSで利用できるさまざまな暗号技術の概要
• TLSをウェブで利用するためのHTTPS（Hypertext Transfer Protocol Secure）
• そのための社会的な技術基盤としてのPKI（Public Key Infrastructure）
• PKIにおける信頼モデルを支える証明書とCA（Certification Authority、認証局）
• プロトコル、PKI、実装の安全性を破る、数々の脆弱性およびインシデントの発見、それらに対抗する研究者と業界をめぐるストーリー
• 現場でいますぐ使えるOpenSSL各種ツールの使いこなし

テストケースはコンピューターで書くべき！ でもどうやって？ その答えが「プロパティベーステスト」です

• Fred Hebert 著、山口能迪 訳
• 原書 Property-Based Testing with PropEr, Erlang, and Elixir
• 376ページ
• A5判
• ISBN：978-4-908686-18-4
• 2023年11月1日 発行

従来のユニットテストでは、人間が「入力に対してコードが返すべき値」を考えて、その通りの結果が得られるかどうかをテストします。 これに対してプロパティベーステストでは、数万にも及ぶ多様なテストケースをコンピューターで自動生成し、その大量のテストを水面下で実行することによって、どんな入力に対してどんな問題が起きるかをテストします。 人間には思いもつかない入力まで網羅できることから、単に手間をかけずにテストケースを増えせるだけでなく、場合によっては仕様に潜むバグさえもあぶり出せる強力なテスト手法です。

プロパティベーステストで人間が記述するのは、「入力に対してコードが返すべき値」ではなく、「入力に対するコードの振る舞い」そのものを表す実行可能なコード（プロパティ）です。プロパティを書くためのアプローチとして、本書では次のような考え方を学びます。

• 通常のユニットテストで人間が書くようなテストケースをランダムに自動生成する
• より単純な機能を使った別の実装を作って比較する
• 不変条件や対称的な操作を見つけてそれを利用する

これらのアプローチ自体は言語に依存しませんが、表現力や実行方法はさまざまな言語で実装されているプロパティベーステストのためのフレームワークに依存します。 本書では、Erlang/Elixirで利用可能なPropErというフレームワークを利用し、上記のような基本的なアプローチによるプロパティベーステストはもちろん、生成したいテストケースが互いに独立でない場合のプロパティベーステストや、状態に依存するシステムに対するプロパティベーステストなど、高度な応用事例についても紹介します。

本格的なアプリケーション開発を通して、プロパティベーステストの基礎から極北までを体験できる、唯一無二の解説書です。