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.