5 ms·

ATS is not really a theorem proving language, it's almost a superset of C with a very long list of type system and language features that lets you write anythin

ATS is not really a theorem proving language, it's almost a superset of C with a very long list of type system and language features that lets you write anything from C code with no safety to very high level recursive functional code with lifetime tracking which will translate to efficient C code, if the transformations are proved to be correct. It's a weird beast, but I'm not surprised it outperformed some C implementations, because it is basically C with a lot more features.

ghostwriter 6y ago
> ATS is not really a theorem proving language What is "real theorem-proving language" in this context? ATS has ATS/LF that is designed for writing formal proofs in the language. http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/c2867.html http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/...