Well that's totally true, but even then I have no idea what the legal mechanism is for making a formally verified language in the context of a medical device looks like, or even decision support software like the grandparent was discussing.

Even if such a thing existed, it would require a very rich set of constraints on the program to be able to encode something like "won't make the wrong decision when a patient has a pulmonary embolism and these three other conditions" and I think that's what doctors would want.

Formal verification is a barrier to quick iteration (parent comment) not just for medical software, but anything "mission critical" where the mission is "worst case scenario, don't kill someone". Hence my point about train switching and avionics. Legal mechanisms are beside the point, I think.

As for rich constraints, that does bring up another point- how do you quickly iterate on a system full of bad data or systems of incompatible data? To get Watson to a degree of certainty, so much data manipulation and review happened by hand that it was a wasted effort.

This isn't to say that I'm in love with what I've seen of the software my doctors use (or the puckering feeling seeing how outdated the OS tends to be). I'd be a whole lot less happy, though, if their software had the reliability of say, imgur or reddit.

> Safety first, full stop, no exceptions.

And here you are, cutting-edg hospitals running 2012 versions of modern software, and paying millions of dollars for the privilege.

The direction has to be exactly the opposite, by giving the patient increasingly more control over his own health.

Having seen several talks from some patient advocates recently, I'm skeptical that's a good idea.

I think health services are some of the most misunderstood by the population above everything else.

Patients are the worst at their own health, and often deluded about their ability to manage it. Gwyneth Paltrow and homeopaths don’t rake in money because people make great decisions. When you “empower” patients past their competence you get Steve Jobs in the ground. If he had just been another schmuck, he’d probably still be alive.

Health services are in service of the patients, not on your commoner opinion of what health should be and how it should be imparted.

And being in service of the patient often requires not doing what the patient wants, because the patient is not a medical professional and doesn't know shit.

Most people taking homeopathic medicine want their symptoms to get better. It’s not as though they have some different definition of a “good health outcome,” they’re just mislead about the effects of the what they’re buying.

Placebos work. Sad but true.

   Coq but with the ease of 
   Java or Typescript

Don't hold your breath. There is currently no technology on the horizon that holds a promise to bring use even close to what you ask for.

Note also that Coq/Isabelle/Agda and their successors will still suffer from a variant of the oracle problem: where should the specifications come from?

Finally note that almost virtually aviation software is formally verified in with interactive theorem proving as of 2018. The extreme levels of reliability in this space have always been achieved with other software engineering methods, including rigorous testing.

I was thinking more of that would be (a or the) barrier to rapid iteration in medical software, not that it is likely to be achievable. Given the rigorous testing required in its place, we don't get web dev agile style iteration in medical software.

I don't think safety issues are preventing anything here. You don't have to iterate on live systems or real patients. You can test and develop on mockups and simulated scenarios taken straight from real life. But you need to be able to get regular feedback from actual end-users.