>I hope for a future where programmers will be able to specify all contracts, invariants, etc. in code
Theoretically is this even possible? We simulate this with tests, and code-coverage analysis, but in the end all programs deal with unknown inputs, by definition.