Re:Go bindings to Rust's regex engine
by nickpsecurity on Wednesday May 04, 2016 @07:17AM
(#11627540)
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...
My goal is correctness. A program that fails with a runtime exception is just as wrong as another that silently corrupts your data. Dijkstra put it very nicely:
“We could, for instance, begin with cleaning up our language by no longer calling a bug a bug but by calling it an error. (...) The nice thing of this simple change of vocabulary is that it has such a profound effect: while, before, a program with only one bug used to be "almost correct", afterwards a program with an error is just "wrong" (because in error).”
https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/E...