Hacker News new | ask | show | jobs
by philix001 1455 days ago
The spec might not even contain the level of detail necessary for that to be possible. That possibility is what makes modeling easier than implementing the spec.

Through a process of manual refinement, you can derive an implementation from the spec and check every step with the checker, but that's is more work than implementing the formal spec manually and is an most likely an overkill in practice.