The Coq mailing list

[David MENTRÉ <dmentre AT linux-france.org>]

Hello,

Le 2017-10-10 à 20:00, Daniel Schepler a écrit :
> On Tue, Oct 10, 2017 at 10:36 AM, Abhishek Anand
> <abhishek.anand.iitg AT gmail.com>
>  wrote:
>> I am curious what you want to prove about GUIs.

I am sharing this curiosity.


> A while
> ago, somewhere on Wikipedia I read about a situation with control
> software of a radiation therapy device.  Under a certain sequence of
> actions that wasn't anticipated by the software designers, it could
> end up opening all filters which was never supposed to happen,
> resulting in a massive overdose of radiation.

You are probably speaking about Therac 25. Nancy Leveson reports on the
accidents is the best source of information:
  http://sunnyday.mit.edu/papers/therac.pdf

Therac 25 is probably one of the poorest software ever designed
(concurrent routines without real protection), although it is easy to
judge with our modern viewpoint.

Best regards,
david