[mazesc]

Ada is already mentioned here.

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.

[hwayne]

Dafny is a really fun language and I've done some stuff in it before. I was really sad when MSR stopped working on it, but I think AWS has picked up the slack?

[mazesc]

Yes, it's under heavy development, and is getting various improvements for usability. You probably want to take a look at the release notes.

[hwayne]

glee

[UncleEntity]

I kind of thought Coco/R was a dead project but it seems dafny is using it as the parser generator library.

…have to poke around a bit methinks.