4 ms·

There was a long period where a fairly unknown theorem proving language ATS (1) was beating C in many test cases on the benchmark game (2) the benchmarks were r

There was a long period where a fairly unknown theorem proving language ATS (1) was beating C in many test cases on the benchmark game (2) the benchmarks were removed though (3). I expect many languages could be made to win with sufficient effort. 1. http://www.ats-lang.org/ http://www.ats-lang.org/ 2. http://web.archive.org/web/20121218042116/http://shootout.alioth.debian.org/u64/ats.php http://web.archive.org/web/20121218042116/http://shootout.al... 3. https://stackoverflow.com/questions/26958969/why-was-the-ats-language-dropped-from-the-computer-language-benchmarks-game https://stackoverflow.com/questions/26958969/why-was-the-ats...

steinuil 6y ago
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/...