ATS language

https://en.wikipedia.org/wiki/ATS_(programming_language)
As fast as C( http://stackoverflow.com/questions/26958969/why-was-the-ats-language-dropped-from-the-computer-language-benchmarks-game https://www.reddit.com/r/programming/comments/72hmw/language_shootout_ats_is_the_new_top_gunslinger/ )
Dependent types
Safety and built-in theorem proving

>>23
So you're saying that a mathematician or computer scientist who has studied compiler theory and language grammar and formal logic is unable to use these theories together into an application that is a programming language system that can systematically check the semantics of a logical specification within a computer program? You're right, everybody knows that formal verification using computer software is not possible.