What goes into proving two complicated programs are equivalent?

Question

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?

Right now I am just assuming they are equal implicitly, allowing my code to call either the C function or the JS function knowing that the ~overall effect~ is the same (nebulous, I know, don't know how to pin it down). I would like to apply some math or model checking or program simulation or something to this so that I can make it more solid, if possible :)

At the other end of the spectrum is proving that 3 > 2 is equivalent in both C and JS. What am I even supposed to do in this simple case? Making that slightly more complex on it's way to a full HTTP server, copying a string in C is very different than in JavaScript, but it's a relatively simple thing. Where do I even begin to prove those "operations" equivalent between the two languages? Or if not "prove", then just "state" that they are equivalent, with some backup evidence or something, I dunno.

Here is not much, but this diagram is what I'm basically trying to do:

At a broader level, the problem seems to be similar to this.... Say I want to get a medallion. I can either go the store and buy one, or I can 3D print one. Both "algorithms" (going to the store, or 3D printing) are way different from each other, but they are effectively the same. There would be no straightforward way to step-wise prove these are equivalent operationally (from what my imagination provides), but visibly the end result is the same. How would you (even here) state this with rigor?

Answer 1

Formal analysis today is usually done on module or unit level. Unfortunately I'm not aware of a common metric which allows to predict if a formal analysis will be possible. Only structurally very simple codes can be formally analysed even with LOC's or cyclomatic complexities of up to a million.

In your case here the code of any of the two programs is clearly too complex for a full formal analysis:

• Model-checking will not work.
• A complete (bi-) simulation will not work either.

So the best practical solution I know is model-based testing. While it is not a proof still formal methods can be used. It ultimately eliminates the disaster of writing and maintaining manually written test cases.

P.S.:

A short list of steps which can be done in this case:

• An abstract model of the two programs is created. This is a third implementation which will omit all unimportant details. The abstraction has the advantage that this model is simple enough again to be formally analysed. The model can be implemented in any language you like if the model analyser will analyse the byte code.
• The abstract model can be traversed and e.g. a condition coverage is reached in a test suite. This step is done using a model-based-testing tool.
• Finally these test cases are tested on the two programs and it is checked if the abstract model can simulate the two program implementations.
• This simulation relation is of course not a proof of the equivalence.
• The abstraction is a very clean specification what was taken into account in our tests and what was omitted.
• Two model-based testing tools which can be recommended: Microsoft Spec Explorer, Conformiq Designer

Answer 2

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).