formal-proof

TypeScriptでIDなどの特別な数値や文字列を型安全な専用の属性付きプリミティブ型にする

TypeScriptでIDやエンコーディングなど特別なセマンティクスを持つ値にプリミティブ型を維持したまま個別の属性を与えることで型安全な専用の値を作る。言語の型システムをどのように機能させているかについての説明は省略する。 IDは次のように作れる。 nam…

TypeScriptで形式的証明・交差型編 ~ 状態付きの型による高信頼領域の構築

TypeScriptで交差型を使って静的型に状態的な型を動的に付与していきます。 これによりサニタイズ済/未サニタイズ、エンコード済/未エンコード、不変/可変、通常文脈/エラー文脈、Truthy/Falsyといった状態を複合的に扱えるようになります。 さっそく試して…

TypeScriptで形式的証明・直和型編 ~ じゃんけんゲーム最強トーナメント

TypeScriptで形式的証明を取り入れたプログラミングを実践します。 形式的証明とは、仕様またはモデルが数理論理学的に正しいものであり実装可能であることの形式手法による証明です。 本稿では形式手法のうち、型システムを利用した軽量形式手法による形式…