buttondown-com-hillelwayne

「プログラミングに数学は不要」という主張に反論する中で、「すべてのプログラマーが数学を学ぶべきか」という問いを考察。算術や集合など一部の数学は全員に有用だが、それ以外の分野は大多数にはコスパが悪い。ただし、各プログラマーが自分の分野に役立つ数学を見つけるには、様々な分野の「概要」を知ることが重要で、深く学ぶのはその後で良いと論じる。知識の習得において「浅く広い」曝露が最初の一歩として有効だ。

論理的な含意（implication）の観点から、「仮定を追加すると特性（プロパティ）は弱くなる」という原則を解説。JSONパーサーやRustのメモリ安全性、モックテストなどの実例を通じて、なぜ強い特性を直接検証せずに仮定を設けるのか、その理由（実現不可能性、コスト、検証容易性）を説明する。また、仮定の多くがシステム外部要因に依存する点にも言及し、仮定の検証自体がコード検証とは別の難しい課題であることを指摘する。

LaTeXとInkscapeで同じ「ポイント」という単位を使っているのに、実際の長さが異なることに著者は気づいた。LaTeXは1ポイント＝1/72.27インチ、Inkscape（PostScript由来）は1/72インチと定義しており、その差はわずか0.4%だが、歴史的に混乱があった。この記事では、16世紀から現代に至るポイント単位の変遷と、TeX・PostScript・CSS・Frinkなど各技術における定義の違いを詳しく解説している。

プログラマ向け論理学の書籍「Logic for Programmers」v0.14をリリースし、6月末の正式出版（1.0）に向けてテスト印刷も開始。また、著者は8月から生成テストプラットフォーム企業Antithesisにフルタイムで Developer Educator として勤務予定。ニュースレターの内容は形式的検証より歴史やソフトウェアの奇妙な話題にシフトし、更新頻度も週1から隔週や月1に減らす可能性がある。

「非法状態（illegal state）」はシステムが決してあってはならない状態を指し、「望ましくない状態（unwanted state）」は留まりたくないが一時的に発生しうる状態を指す。カレンダーアプリの予定重複や航空会社のオーバーブッキングのように、非法に見えて実は望ましくないだけの状態は多い。システムは外界からの入力や運用上の要件により、望ましくない状態を一時的に許容する必要があり、それが非法状態に発展しないよう検出・解決する仕組みが求められる。

TLA+の理論的な非順序保証と、モデルチェッカーTLCによる実装上の制約（PrintTなどの副作用演算子や変数定義順序の影響）の違いが混乱を招く。宣言的言語の抽象化が漏れ出る典型的な例であり、視覚的に区別できないことが問題を複雑にしている。

論理量化子「すべて」と「いくつか」は、ソフトウェア開発において高レベルのプロパティを表現する重要な手段です。これらはコードパターンの簡略化、データベース不変条件の表現、テスト可能な仕様の明確化など、実用的な場面で活用できます。

Hillel Wayne氏の書籍『Logic for Programmers』がリリースから1周年を迎えました。現在v0.10まで進化し、当初の19,000語から31,000語に拡大、TLA+や制約ソルバーなどの新章も追加されています。セルフパブリッシングで1,180冊を販売し、今後は最終版に向けてさらなる改訂と編集作業が計画されています。

著者はVSCodeからNeovimに戻ったことで生産性が大幅に向上した経験から、コードを書く速度が開発のボトルネックではないという通説に疑問を投げかけています。もしコードを100倍速く書けるようになれば、ボイラープレートの作成、ツール開発、テスト駆動開発の実施、実験的な編集などが劇的に改善され、新しい開発プロセスが可能になると論じています。

プログラミング言語には、言語の核となる仮定を意図的に破って機能を追加する「エスケープハッチ」が存在します。Rustのunsafe、C++のインラインアセンブリ、Rubyのsendなど、パズル言語だけでなく主流言語にも見られる機能ですが、使用は慎重に制限されるべきです。

この記事では、配列を数学的関数としてモデル化する概念的な枠組みを提案し、APLスタイルの多次元配列とデータテーブルの両方を統一的に説明します。構造体の異種性がテーブルの特性を決定し、配列の次元を任意の有限集合として一般化できることを示します。

著者が10年前に欲しかった本『Logic for Programmers』を執筆中であると述べ、ブログ記事よりも書籍の深い影響力に言及。さらに、設定管理、複雑なデータスキーマ、ソフトウェアエンジニアのためのコンピュータサイエンスなど、まだ存在しないが読みたいソフトウェア関連の書籍のアイデアを提案している。

プログラミング言語が思考に与える影響は、サピア・ウォーフ仮説よりも「テトリス効果」で説明できる。特定のスキルを長時間練習することで、そのスキルに関連するパターンが日常生活でも目につくようになる現象だ。プログラミング言語のパラダイムの違いは、特定の思考方法を強制することでこの効果を促進する。

古典論理における演算子の双対性（F(x) = !G(!x)）をソフトウェア工学に応用した考察。特に量化子の双対性（∃x: P(x) ⇔ ¬∀x: ¬P(x)）に着目し、Z3、プロパティテスト、モデルチェッカーなどのツールが一方の機能から他方を導出できる仕組みを解説。SQLの制約やデータベーストリガーにおける実用例も紹介。

非決定性には「悪魔的非決定性」（常に最悪の選択をする）と「天使的非決定性」（常に最善の選択をする）の2種類がある。前者は形式手法で安全性検証に使われ、後者は計算複雑性理論やプログラミング言語で広く用いられる。NP問題は天使的非決定性を持つ多項式時間アルゴリズムで解ける問題として定義される。

動的計画法などの複雑なアルゴリズムを必要とする難しいLeetCode問題の多くは、MiniZincなどの制約ソルバーを使えば簡単に解決できます。著者は、コイン両替問題や株価最大化問題などの例を示し、プログラミング言語で直接アルゴリズムを書くよりも制約ソルバーを使用する方が効率的で柔軟な解決策が得られると主張しています。

Hillel Wayne氏が、代数的データ型の起源を探る3500語の詳細なブログ記事を公開しました。当初はニュースレターで簡潔な歴史を紹介する予定でしたが、内容が膨らんで完全な記事となりました。記事では、この重要なプログラミング概念の初期の発展を掘り下げています。

形式的検証済みコードが実際にバグを持つ可能性がある3つの主要な方法を解説：証明の無効性、仕様の不備、前提条件の誤り。特に「Let's Prove Leftpad」プロジェクトの例を通じて、Unicode処理の微妙な問題や、仕様と実際の要件の乖離がどのようにバグを生むかを示す。

著者は初めて10kmを走った経験から、学習やスキル習得における「相転移」現象について考察する。ランニングやプログラミング言語の習得において、進歩は連続的ではなく、ある時点で突然「できる」という段階にジャンプする。この相転移を早めることは可能か、あるいは相転移が起こるまで継続する動機づけをいかに提供するかについて論じている。

モーダル編集（Vimなど）は、その利点が明白ではないにもかかわらず、viが無料で広く配布された歴史的偶然によって現在まで存続している。もしBill Joyがviを作らなければ、今日モーダルエディタは存在しなかっただろう。

Hillel Wayne氏は、週刊ソフトウェアエッセイの執筆による燃え尽き症候群を理由に、今年いっぱい『Computer Things』の執筆を休止すると発表しました。週刊ペースでの執筆再開は2026年まで行わない予定です。

今月末まで、クーポンコード「feedchicago」で「プログラマーのための論理学」を半額で購入できます。このクーポンによるすべての印税は、グレーター・シカゴ・フード・デポジトリーに寄付されます。

『プログラマのための論理学』電子書籍を50%オフで購入すると、印税全額がシカゴ地域のフードバンクに寄付されるキャンペーンが11月末まで実施中。これまでに1600ドル以上が集まり、目標の2000ドルを目指している。

この記事では、ソフトウェアに関する興味深い事実を紹介しています。例えば、2017年に8人以上のプログラマーチームがライフゲームシミュレーション内でテトリスを実装したこと、Vimがチューリング完全であること、クラウドフレアがランダム数生成に溶岩ランプの写真を使用していることなど、様々な技術的なトリビアが取り上げられています。

リスコフの置換原則は単なるサブタイピング以上のものであり、メソッドの事前条件と事後条件に関する契約の観点から、継承に限定されず、コードの置換全般に適用できる。APIの変更やバージョン管理においても、事前条件を弱め、事後条件を強めることで互換性を保証できるが、ハイラムの法則により明示的な契約の重要性が示される。

著者はPrologの欠点について、標準化された文字列型の欠如、関数の不在、リスト以外の標準コレクション型の不足、真偽値の欠如、カットの混乱、否定の扱いの難しさ、クエリの複雑さ、記号項の扱い、sortの挙動、ルール末尾のピリオドの煩わしさなどを挙げている。これらの問題点を踏まえ、著者は論理プログラミングのニーズにはPicatを好むと述べている。

SQLデータベースのブール型カラムを日時型に移行する際、外部コードを変更せずにリファインメントマッピングを使用して互換性を維持する方法を解説。イベントソーシングへの移行や不変性制約の扱いも含め、データベースの文脈でリファインメントの概念を説明する。

プログラマーのための論理学の新バージョンv0.13がリリースされました。全章が書き直され、Alloyの章はデータモデリングからドメインモデリングへと根本的に変更されました。今後は編集、校正、レイアウト調整を経て、夏までに物理書籍として完成させる予定です。

形式手法コンサルタントとして、システムの特性を数学的に表現する際に使用する「常に真」(A)と「最終的に真」(E)という2つの時間演算子に加えて、第三のクラスとして「可能性」(P)特性を紹介。P(x)は「モデル内でxが発生し得るか」を表し、仕様の妥当性チェックなどに有用だが、AlloyやTLA+などの主要形式手法ではネイティブサポートされていない。

仕様書の修正時に、問題の要約から詳細な説明、解決策の理論と実装方法までをマークダウンファイルに書き出し、思考の流れを可視化する手法。経験差のあるペアプログラミングで、複雑な概念を共有し理解を深めることを目的としている。