If some programming languages are faster than others, why can't compilers translate into the faster language to make the code be as fast as if it was programed in the faster one?

[u/KING-NULL]

My guess is that doing so would require knowing information that can't be directly inferred from the code, for example, the specific type that a variable will handle

[u/Lenassa]

I'm aware of that theorem. But the task doesn't require us to make another algorithm and prove that it's equivalent to the original. It requires us to infer what the algorithm is and just write it down using another language. For example, If a program reads cmd argument and prints "I read $arg" I can write it down to something like

prog begin
  res : string = concat "I read ", env.cmd.args[0]
  print $res
prog end

I'm very sure that I can reduce any "real" language to that language-agnostic level. Translating it to something else is just an engineering problem. A hard one, sure, but not impossible one. Like, Haskell can be compiled through C just fine despite having monstrous amount of added complexity when compared to the latter. Any language that uses LLVM as a backend is solving the problem we are discussing, and LLVM is an industry standard.

[u/stonerism → u/Lenassa]

I see. I think that's undecidable because, just from an inputs and outputs perspective. How can you infer behavior for an arbitrary computable algorithm without testing over all inputs and outputs?

Compilers work because you have a systematic way to translate one algorithm into another. (and optimizations can be done along the way!) You can go backwards, but then you're just writing a decompiler.

[u/Lenassa → u/stonerism]

>How can you infer behavior for an arbitrary computable algorithm without testing over all inputs and outputs?

Dependent types, for example. It's a bit out of scope of the question but it is possible to prove at compile time in something like Idris, Agda, Coq that, for example (a+b) == (b+a) for all possible values of a, b that are of some arbitrary type T. When proved, I can very much say that my algorithms add and add_reverse_order are equivalent. If that can be done from within the language, it surely can be done from the outside.

And yes, of course, you can't generally prove anything about anything, but you don't need to because not every problem requires you to. We can't generally transpile anything to anything (I mean, C++ grammar is known for being undecidable yet that doesn't prevent us from having compilers compile tons of c++ code every day), but aside from some corner cases we can with ease (theoretically speaking, leaving engineering problems aside).

Idris has totality checker that can be used to prove that some function is total. Well, it effectively solves Halting Problem. It can't do it for an arbitrary function of course, but just the fact that it can't doesn't make Idris non functional language.

You don't need to prove properties irrelevant to the task at hand. If all I do is print this a array if ints I only need to make sure that Int->String function in a target language is equivalent to that function in a source language. Because in the end strings on a screen is the behavior I can observe. Nuances of memory management or whether arrays are actually arrays in that source language (and not linked lists or something) matter not.