Probably SPARK (programming language derived from Ada with advanced proof capabilities). The next release of SPARK will support pointer ownership similar to th

Probably SPARK (programming language derived from Ada with advanced proof capabilities). The next release of SPARK will support pointer ownership similar to the Rust borrow checker: https://blog.adacore.com/using-pointers-in-spark https://blog.adacore.com/using-pointers-in-spark https://arxiv.org/pdf/1710.07047.pdf https://arxiv.org/pdf/1710.07047.pdf Concurrency in Ada is very easy. I haven't used SPARK enough to be familiar with its concurrency, but it looks very similar to Ada, but with added restrictions to allow for proofs: https://docs.adacore.com/spark2014-docs/html/ug/en/source/concurrency.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/co...