> You do realize that there can’t be a Turing-complete language that can be formally verified? This is mistaken. Formal verification systems of Turing-complete

> You do realize that there can’t be a Turing-complete language that can be formally verified? This is mistaken. Formal verification systems of Turing-complete languages are indeed subject to Rice's theorem, [0] but these systems don't make a claim of totality, i.e. they aren't claiming to always be able to prove all the properties which are true of a program. Further reading on SPARK: [1][2][3]. > I don’t see why is it problematic to provide a well-defined subset with stricter guarantees while still having the overall language for parts that need the full computational power of Turing machines. If you're going to make use of parts of the Ada language for which there is no formal model, then your solution is at best going to be partially formally verified. That's not necessarily a bad idea, and you can combine formally verified SPARK with unverified Ada code, but it's also possible to write your whole program in verified SPARK. (That's not to say it's easy/cheap to accomplish at scale. Formal development methodologies are notoriously laborious.) Using a non-Turing-complete subset of Ada for solving certain problems doesn't strike me as a bad idea necessarily, but it's not the route SPARK goes. I'm not an expert but I believe verification of non-Turing-complete languages is an active area of research, although I think these languages tend to have a functional flavour. [0] https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem [1] https://www.adacore.com/about-spark https://www.adacore.com/about-spark [2] https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html [3] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)