buttondown-com-hillelwayne

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

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+などの主要形式手法ではネイティブサポートされていない。

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

Hillel Wayne氏が5ヶ月ぶりにブログを更新し、Z3定理証明器で書いたいくつかのシンプルなスクリプトを紹介しています。この投稿では、書籍『Logic for Programmers』の制作中に生まれた「チャフ」（未使用の素材）についても触れ、SMTソルバーの特性や制約について考察しています。

今週は多忙なためニュースレターはお休みします。お詫びとして『Logic for Programmers』の無料コピーを10部提供します。5部は現在入手可能で、残り5部は明日10:30 CESTから利用可能になる予定でしたが、Leanpubのバグにより実現しませんでした。

LLMが生成する形式的仕様書は、実際に検証を行うべき「微妙な」性質を捉えるのが苦手であり、自明な性質しか書けない傾向がある。初心者がAIを使って形式的仕様を書こうとすると、コンパイルすらできないコードや、実質的に何も検証しないアサーションが生成されることが多い。形式的メソッドの専門家でなければ、LLMから有用な仕様を引き出すのは難しいという問題がある。

新しい技術には未知のリスクと長期的な保守負担があるため、技術選択は保守的に行うべきです。一方、開発プラクティスは導入・廃止が容易なので、より自由に革新を追求できます。技術を「素材」と「ツール」に分け、素材は安定を、ツールは革新を重視するアプローチが提案されています。

この投稿では、ニューヨークとシカゴのピザ論争に新たな視点を提供し、特にシカゴの深皿ピザと詰め込みピザの違いについて考察しています。著者は、この論争よりもシカゴが素晴らしいソーセージの街であることを強調しています。

仕様は可能な実装の集合に対応し、コードはその集合内の単一の実装である。十分に詳細な仕様であっても、それはコードではなく、実装の抽象化として捉えるべきだ。仕様とコードを区別することで、両者の役割を明確に理解できる。