セッションのテーマ

• 言語

  想定する聴衆/前提知識

• 誰でも

概要

The behavior space model [1] classifies software behaviors by whether they are specified (Sv, Su) or unspecified (Ev, Eu). We apply this model to type systems. Static type systems generate Sv automatically —
every type declaration is a compiler-verified specification. Behaviors derived beyond explicit intent
constitute Ev, but unlike test-based Ev, they require zero human management cost. Dynamic languages force all type-level verification into linear-cost test-based Ev. Gradual type systems (TypeScript, Python
type hints) are structurally more hazardous than either: Sv and E are expressed in identical syntax,
rendering their boundary invisible within the same codebase. Under AI-assisted development, where code
generation volume makes language-level Sv yield an organizational infrastructure question, these
structural differences become critical.

https://doi.org/10.5281/zenodo.18752758