ご来店ありがとうございます。
開店以来およそ6ヶ月、ここまで『プロフェッショナルSSL/TLS』と『RubyでつくるRuby』の2タイトルで営業していたラムダノートのWebサイトですが、 久しぶりに新刊の発売を開始します。しかも2タイトルの同時発売です！
1つめの新刊タイトルは『定理証明手習い』です。 証明といっても、証明するのは数学の定理ではなくプログラムの正しさです。 
プログラムの正しさというと、まだまだテストによる検証などが真っ先に思い浮かぶかもしれません。しかし、たとえば「定義した関数があらゆる入力に対して破綻せずに動作するか」をユニットテストだけで検証しつくすことはできません。
そこで、数学で公理から推論規則だけで命題の正しさを証明するように、プログラムでも公理からの等価な書き換えのみで関数の正しさを証明しようというのが、定理証明です。 どんなプログラムについてどんな正しさが証明可能なのか、どんな手順で証明を進めるのか、そういう証明の一部を手助けしてくれるプログラム（定理証明支援系と呼ばれます）は作れないものなのか、というのが本書の主な内容になります。
CoqやAgdaといった定理証明支援系の名前は聞いたことがあるけど、そもそも定理証明ってなんなのかよくわからない、でもプログラムの正しさを証明できるってなんだか素敵だ、という方にぴったりの教科書です。『Scheme手習い』でおなじみのDaniel P. Friedmanと、Carl Eastlundによるユニークな原著を、中野圭介さんに監訳していただき、これからますます注目されるであろう定理証明を扱った日本語の書籍として正確かつ読みやすい本になっています。
もう1つの新刊タイトルは、『Goならわかるシステムプログラミング』です。 こちらは、ASCII.jpで連載していた渋川よしきさんの同名の連載の書籍化になります。
OSの機能をひととおり網羅する教科書でありながら、C言語ではなくGo言語を用いた実動するコードで解説しているという、まさに21世紀のシステムプログラミング本といえる内容になっています。 システムプログラミングといって想像されるような、OSやデバイスドライバを自作したいような人向けというよりも、ふだんはWebアプリケーションを書いているけれど低レイヤのことも少し知っておきたい方にぴったりの教科書です。
Goによるシンプルかつ適度に抽象化されたサンプルコードと、Web連載時からさらにブラッシュアップしたイラスト、それにサービス精神がありすぎる渋川さんの解説により、従来の入門書ではとっつきにくい話題や、取り上げられていないような新しい話題も楽しんでいただける一冊です。
どちらの書籍も、ラムダノートのサイトでの直販に加えて、10月下旬から書店店頭やオンライン書店でも購入できる予定です。さらに、10/22（日）の「技術書典3」での先行販売を予定しています！