What goes into proving two complicated programs are equivalent?

Say I wanted to prove that two programs were equivalent (either rigorously if possible, or informally if not). More specifically, say I have something relatively complex such as an HTTP server implemented in C, and one implemented in Node.js/JavaScript. What can I do in terms of saying "these two are effectively the same"? What are my options? What is possible? What is not possible?

It's been a little while since I've looked into proving program equivalence (I'm currently linked to this, but I can't read it yet haha, and it looks like it's focusing on extremely simple programs like equality checks or basic loops, whereas I'm asking about a robust HTTP server).

Essentially (I'm imagining) I want to say "these two programs in JS and C do the same thing". That "do the same thing" is obviously vague, but at the same time it means something specific. Any observable outcome on either system is generally the same, give or take. So it's like a proof, but without being a perfect proof. It's like it's a partial proof or something.

I would like to be able to say of my programs "these two implementations are equivalent for all intents and purposes". I would probably start by providing measurable guarantees or observations about performance and input/output behavior, and then write some tests, and ... I don't quite remember, somehow make statements about the system. Or should I just be thinking that "a functioning HTTP server in either language is an AXIOM". That would simplify it :) Just assume it does the same thing as one another. But that's sidestepping it feels like.

Wondering what are my options here? How far can I take this in theory? I am not concerned with how long this would take to implement or define, if it takes years, fine. I just would like to know what is possible in terms of making the statement "these two programs in C and JS are equivalent" more rigorous and nailed down. What techniques/theories/research-directions could I look into to make it possible?

R

One could write an entire book surveying techniques of proving program equivalence. This answer is just as a very short starting point:

Theoretically, if you think about your programs as Turing Machines, then all hope is lost -- proving that two TMs have the same language (i.e., they are semantically equivalent) is undecidable (in fact, it's not in RE$\cup$ coRE).

Still theoretically, if you think about your programs as finite state machines, by including the states of the memory as part of the machine, then program equivalence for DFAs is very simple (solvable in NL), and for NFAs it's PSPACE complete. The problem with this approach is that the state space would be huge (e.g., if you have only 100 bits of memory, your state space has at least $2^{100}$ states), so this is unreasonable.

Now that we've cleared the theoretical bounds, there is an immense body of work addressing these topics, including ways to define operational semantics.

Basically, this is the field of Formal Verification, and just some keywords that can get you started:

• Model checking

• Bisimulation

• Abstraction - Refinement

• Theorem Provers (e.g., Coq)

Note that in practice, many companies are formally verifying their code. For hardware, this is common practice, and is an important stage in development. For software, the huge complexity means that only small bits of code are getting proved formally, never entire programs (not yet, at least).

StackExchange Computer Science Q#118835, answer score: 4