When Formal Systems Kill: Computer Ethics and Formal Methods
Darren Abramson, Lee Pike · 2011
“Beware of bugs in the above code; I have only proved it correct, not tried it.” —Donald Knuth “Program testing can be a very effective way to show the presence of bugs, but is hopelessly inadequate for showing their absence.” —Edsger Dijkstra Computers are different from all other artifacts in that they are automatic formal systems. Since computers are automatic formal systems, techniques called formal methods can be used to help ensure their safety. First, we call upon practitioners of computer ethics to deliberate over when the application of formal methods to computing systems is a moral obligation. To support this deliberation, we provide a primer of the subfield of computer science called formal methods for non-specialists. Second, we give a few arguments in favor of bringing discussions of formal methods into the fold of computer ethics.