It's very useful for things where the specification is much simpler than the implementation. Databases and file systems are good examples. A database can be spe

It's very useful for things where the specification is much simpler than the implementation. Databases and file systems are good examples. A database can be specified as giant arrays with linear search. Now prove that the database with all its optimizations and concurrency behaves the same as the simple spec.