"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."
(dose > MAX_DOSE) ? return DOSE_TOO_HIGH : return DOSE_ACCEPTED;
20 units is obviously dangerous for a single dose.
Stranding users who use the app without access to our lifesaving medical device is... Bold, to say the least.
https://www.northwoodsendocrinology.com/wp-content/uploads/2...
Presumably whoever provided you your pump has a similar instruction.
Risking using an app/pump combo that has a known flaw, especially a non-deterministic one is bold, to say the least. Safer to switch to the regular controller (assuming you have it) until this is fixed.
The users phone could be stolen, or the device compromised, or many other things. A compromised device should not be able to cause physical harm to a human!
edit: someone else already said basically the same thing but I didn't see it because I opened this tab a long time ago and didn't refresh it!
The actual device (not the app) does seem poorly engineered and not at all fail safe / provided with ‘might kill the patient’ error handling.
Seems like double whammy where an app and hardware conspire against its user.
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.
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.
To put it into perspective (at least with my insulin to carb ratio, it varies from person to person), if you wanted to drink a regular sized can of coke, you would dose 3.3u. 66u is therefore enough insulin for 20 cans of coke.
Another way to put it is that 10g of sugar ~ 1u of insulin. You'd have to eat 660g of raw sugar.
There is a medication called Glucagen which is used to treat severe hypo. It works by triggering release of stored glucose from the liver. The thing is, from what I've quickly googled, a typical 1mg dose is usually only enough to raise your blood sugar by about 100mg/dl, and then your store is depleted and further doses have no effect. With my insulin/carb ratio, I would only need about 2.5u to reduce my blood sugar by 100mg/dl.
All of a sudden it feels scary to think that the reservoir in my pump holds about 300u of insulin...
In the days before I had a pump I did something similar to myself. I had a short acting insulin and long acting insulin both in pen form. Managed to give myself the large overnight dose which should have been the long acting with the short acting pen. After about 15 minutes I realized something was up when I felt the low coming on and spent the next 2 hours drinking a disgusting amount of orange juice.
I have had exactly the same experience. One glass of orange juice is great. 3/4 of a gallon.. not so much.