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
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?