Cute quote by Dijkstra that shows he hadn't quite figured out reality yet. So, correctness is your goal. That means you'll have to specify the behavior, safety/security policy, and prove the two equivalent. The implementation, both source and binary, will have to be shown equivalent along with proven free of language-level issues. Finally, you have to do that on triple, modular hardware [1] that's rad-hard w/ similar rigor in its lifecycle. Or use run-time checks [2] for each algorithm that can correct errors probably also on TMR or rad-hard board. Let's not forget the custom circuitry for RAM that works [3].

Darn, Dijkstra or not, you still need some kind of runtime checks and protection for correctness. :)

[1] http://www.rockwellcollins.com/~/media/Files/Unsecure/Produc...

[2] https://galois.com/project/copilot/

[3] https://research.google.com/pubs/pub35162.html