You also want to look at Dafny for a contract-based language: https://github.com/dafny-lang/dafny
Since it has verification support it also covers the second point about semantic relations.
…have to poke around a bit methinks.
You also want to look at Dafny for a contract-based language: https://github.com/dafny-lang/dafny
Since it has verification support it also covers the second point about semantic relations.