Home

When Formal Systems Kill: Computer Ethics and Formal Methods

While ethics aren't normal LtU fare, it's sometimes interesting to see how our technical discussions fit into a larger picture.

In When Formal Systems Kill: Computer Ethics and Formal Methods February, 2012, Darren Abramson and Lee Pike make the case that the ubiquity of computing in safety critical systems and systems that can create real economic harm means that formal methods should not just be technical and economic discussions but ethical ones as well.

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.

They also spend a good amount of time giving a lay overview of the practical, economic challenges faced by formal methods.

By James Iry at 2012-02-24 18:58 | Admin | General | other blogs | 12865 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Worrydreams and Principles

There was an excellent video, Inventing on Principle, in which Bret Victor describes the ethical dilemma some people might perceive.

a guiding principle for your work, something that you believe is important, necessary, and right [...]

because ideas are so precious to me, when I see this principle violated, when I see ideas stillborn or stunted because their creator couldn't see what they were doing, I feel that's wrong. And not wrong in the sense of violating some UI guideline or going against a best practice, but wrong in a deeper sense then that

It is truly an excellent video. I recommend it to everyone.

Regarding the topic, I believe there are many properties that trump safety or correctness. Consistency, for example - it is better to be deterministically wrong than unpredictably right, due to how it impacts maintenance and composition. And resilience, e.g. crash-only software with good recovery has many advantages over safe, robust software (not least of which advantages regard live maintenance and upgrade). Similarly, I would reject specific formal methods if the methods in question violated principles of secure interaction design - e.g. methods based on global whitebox reasoning.

By dmbarbour at Fri, 2012-02-24 22:51 | login or register to post comments

Off topic, a bit, but the

Off topic, a bit, but the wiki page only mentions Erlang as a language where crash-only is an integral part of designing software in it. Do you know of any other languages where it is as core?

By orbitz at Wed, 2012-02-29 21:13 | login or register to post comments

Crash-only

I don't know of many languages that make it part of the community discipline, but I have read about mission-critical real-time embedded systems that simply go the route of running a program and terminating it per `round`. And the entire REST architectural style is aligned well with crash-only servers.

By dmbarbour at Wed, 2012-02-29 23:02 | login or register to post comments

No GNU, since it is too risky?

Hi,

No GNU I guess:

“Patents are a way to convey to management that we are an innovative program. What you've done is particularly unique and will provide leverage with [our external partners].”

- Anonymous (why?) government client
http://corp.galois.com/services/

Galois values the privacy of our customers and partners. We love helping organizations communicate and collaborate, but at the end of the day, you are in control of how you communicate your information, your intellectual property, and your computer security risks. Have we had an impact on your organization? Email us with a quote to add to our web site.
http://corp.galois.com/why-are-quotes-anonymous

Bottom line (Just a guess): Exposing proofs could increase vulnerability of systems, for example since the proofs represent certain assumptions. Not sure how this dilemma could be solved?

Only expose supposedly mature systems? What if the environment changes and makes the system immature? How widthdraw? (Android being an example, what is exposed as SDK is always lacking what is cooking, but no formal methods seen)

Bye

By j4n bur53 at Sat, 2012-02-25 11:29 | login or register to post comments

Formal Ethics

Noteworthy, also, are attempts to formalize ethics. In theory, program code could be verified against ethical specifications encoded somehow. I remember seeing a DRM system at the type level in some SIGPLAN publication (possibly this); I've also heard of systems for deductive formal ethics used to verify robot behavior before its executon (here).

Anyway, there are a couple of readable formal ethics books aimed at philosophers (here and here); these strongly resemble LTL and CTL, so much so that knowing the ethical semantics of LTL/CTL syntax made them easier to learn (for me).

EDIT: Changed links which pointed to Google Scholar bibtex citations; those must be specific to my user session.

By aed at Sun, 2012-02-26 01:26 | login or register to post comments

Non of your links works in

Non of your links works in my Firefox 10.0.2, which just might be automatically punished according to the rules.

By Kay Schluehr at Sun, 2012-02-26 03:38 | login or register to post comments

403

Forbidden. Not a Firefox or browser issue. (I'm using Chrome.)

By dmbarbour at Sun, 2012-02-26 03:48 | login or register to post comments