The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Probably relevant:

http://neutrons.uwplse.org/

- Valentin

On 10 October 2017 at 11:00, Daniel Schepler <dschepler AT gmail.com> wrote:

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.
>
> In the healthcare domain, I guess privacy is the biggest concern.

I was thinking correctness of things like recommended medication
doses, or if it's an interface to medical equipment, then verifying
that certain dangerous operating conditions never happen.  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.  (Of course, the rest of
what you wrote also applies here - in that particular situation, the
recommendation was to design hardware interlocks so that it would be
physically impossible for the software to accidentally leave all
filters open and still activate the radiation.)
--
Daniel