Refinement without Specification
This title could be clearer and more informative.Try out Clickbait Shieldfor free (5 uses left this month).
Formal refinement — a technique from formal specification where one system is shown to be a valid implementation of another — is illustrated using familiar SQL database migrations. Starting with a boolean `is_activated` column, the post walks through two successive schema migrations (to a nullable `activated_at` timestamp, then to an event-sourcing model) and shows how refinement mappings can prove each migration preserves external behavior. It then introduces mutability constraints and shows cases where refinement breaks down (e.g., when deactivation events allow reverting activation state). The key insight is that refinement may be easier to teach in a database context rather than alongside formal methods from scratch.
