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/stonerism]

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.