When I read "contract-based language"I immediately thought of Ada. I could be wrong but I think SPARK is incorporated into the Ada 2022 standard at this point,

When I read "contract-based language"I immediately thought of Ada. I could be wrong but I think SPARK is incorporated into the Ada 2022 standard at this point, it could really be thought of as part of the language. It's the furthest thing from a "dynamically typed language" but it can probably also check the "math" requirement here too.