My insulin pump controller has a bug • Hacker News Board

Re: My insulin pump controller has a bug

#81

Post by randomdata » Fri, Dec 01, 2023, 2:09 PM UTC

stalfosknight wrote: post #71

cypherpunks01 wrote: post #58

"We understand this may impact your experience and are here to support you." I love this - I've never heard the euphemism impact your experience used to mean that your life may end . What a wild PR assignment (language off the company's safety notice https://www.omnipod.com/en-gb/fsn-11-2023 )

Why do so many people / companies insist on using grossly euphemistic managerspeak like this?

Like all business communication (and communication in general, really): Fashion. While you occasionally find some trailblazers to set what is new in fashion, mostly people just copy what other people are doing.

Re: My insulin pump controller has a bug

#82

Post by auggierose » Fri, Dec 01, 2023, 2:13 PM UTC

mtmail wrote: post #2

Non-twitter link: https://nitter.net/morganherlocker/status/173045572181552742... (edit: I'm not the author) "Notified today that my insulin pump controller has a bug where the leading decimal point will be dropped, ie: changing a dose of .21 units to 21 units. I can reproduce randomly ~1 in 5 times so probably a race condition. Easily one of the worst software bugs I have ever heard of."

For software like that, not sure how anything other than formally proven correct software is acceptable. And note, no type system is gonna help you with a bug like that.

Re: My insulin pump controller has a bug

#83

Post by layer8 » Fri, Dec 01, 2023, 2:14 PM UTC

cypherpunks01 wrote: post #58

"We understand this may impact your experience and are here to support you." I love this - I've never heard the euphemism impact your experience used to mean that your life may end . What a wild PR assignment (language off the company's safety notice https://www.omnipod.com/en-gb/fsn-11-2023 )

They probably literally meant impact your having an experience, not impact the content of your experience. ;)

Re: My insulin pump controller has a bug

#84

Post by layer8 » Fri, Dec 01, 2023, 2:17 PM UTC

auggierose wrote: post #82

mtmail wrote: post #2

Non-twitter link: https://nitter.net/morganherlocker/status/173045572181552742... (edit: I'm not the author) "Notified today that my insulin pump controller has a bug where the leading decimal point will be dropped, ie: changing a dose of .21 units to 21 units. I can reproduce randomly ~1 in 5 times so probably a race condition. Easily one of the worst software bugs I have ever heard of."

For software like that, not sure how anything other than formally proven correct software is acceptable. And note, no type system is gonna help you with a bug like that.

With the right type system, any formal proof can be represented in it, and the type checker will verify the proof. Any fault that remains can also remain with a formal proof. Look up Curry–Howard isomorphism.

Re: My insulin pump controller has a bug

#85

Post by e2le » Fri, Dec 01, 2023, 2:17 PM UTC

mtmail wrote: post #2

Non-twitter link: https://nitter.net/morganherlocker/status/173045572181552742... (edit: I'm not the author) "Notified today that my insulin pump controller has a bug where the leading decimal point will be dropped, ie: changing a dose of .21 units to 21 units. I can reproduce randomly ~1 in 5 times so probably a race condition. Easily one of the worst software bugs I have ever heard of."

It sounds like the bug was in the Android app. Shouldn't the microcontroller (on the pump) be validating dose values received?

(dose > MAX_DOSE) ? return DOSE_TOO_HIGH : return DOSE_ACCEPTED;

20 units is obviously dangerous for a single dose.

Re: My insulin pump controller has a bug

#86

Post by schiffern » Fri, Dec 01, 2023, 2:19 PM UTC

patagurbon wrote: post #14

This is the Omnipod 5 when using the Android app as the controller. I received the email this morning. This is indeed a pretty terrible bug. I'm hopeful the confirmation screen prevented any real harm from being done. E: I can reproduce. It seems to happen around 1 in 10 entries for me.

  >I'm hopeful the confirmation screen prevented any real harm from being done.

I hope so too, but I doubt it.

Confirmation screens are notorious for becoming habituated and then ignored. Yes, even important ones.

https://alistapart.com/article/neveruseawarning/

Re: My insulin pump controller has a bug

#87

Post by shp0ngle » Fri, Dec 01, 2023, 2:19 PM UTC

stalfosknight wrote: post #71

cypherpunks01 wrote: post #58

"We understand this may impact your experience and are here to support you." I love this - I've never heard the euphemism impact your experience used to mean that your life may end . What a wild PR assignment (language off the company's safety notice https://www.omnipod.com/en-gb/fsn-11-2023 )

Why do so many people / companies insist on using grossly euphemistic managerspeak like this?

liability

Re: My insulin pump controller has a bug

#88

Post by auggierose » Fri, Dec 01, 2023, 2:20 PM UTC

layer8 wrote: post #84

auggierose wrote: post #82

Earlier quoted context omitted.

For software like that, not sure how anything other than formally proven correct software is acceptable. And note, no type system is gonna help you with a bug like that.

With the right type system, any formal proof can be represented in it, and the type checker will verify the proof. Any fault that remains can also remain with a formal proof. Look up Curry–Howard isomorphism.

Obviously I mean an ML-like type system with automatic inference. Otherwise it is just general logic, and you definitely don't need types for that.

And Curry-Howard is the most overrated isomorphism in history. It may make computer scientists head explode, but mathematicians can live without it.

And yes, I know that Lean is based on it, and Tao is using it, and he just doesn't know better. Sorry.

Re: My insulin pump controller has a bug

#89

Post by jacquesm » Fri, Dec 01, 2023, 2:21 PM UTC

e2le wrote: post #85

mtmail wrote: post #2

Non-twitter link: https://nitter.net/morganherlocker/status/173045572181552742... (edit: I'm not the author) "Notified today that my insulin pump controller has a bug where the leading decimal point will be dropped, ie: changing a dose of .21 units to 21 units. I can reproduce randomly ~1 in 5 times so probably a race condition. Easily one of the worst software bugs I have ever heard of."

It sounds like the bug was in the Android app. Shouldn't the microcontroller (on the pump) be validating dose values received? (dose > MAX_DOSE) ? return DOSE_TOO_HIGH : return DOSE_ACCEPTED; 20 units is obviously dangerous for a single dose.

Absolutely. The App should be considered hostile by the pump firmware until proven otherwise.

Re: My insulin pump controller has a bug

#90

Post by layer8 » Fri, Dec 01, 2023, 2:22 PM UTC

auggierose wrote: post #88

layer8 wrote: post #84

Earlier quoted context omitted.

With the right type system, any formal proof can be represented in it, and the type checker will verify the proof. Any fault that remains can also remain with a formal proof. Look up Curry–Howard isomorphism.

Obviously I mean an ML-like type system with automatic inference. Otherwise it is just general logic, and you definitely don't need types for that. And Curry-Howard is the most overrated isomorphism in history. It may make computer scientists head explode, but mathematicians can live without it. And yes, I know that Lean is based on it, and Tao is using it, and he just doesn't know better. Sorry.

Type inference is largely orthogonal to the question.

The point is, any formal proof you could do outside a type system you can also do within a type system, so yes the right type system would help you avoid such bugs.