Re: Lobotomies....
"Surely someone a has a chunk of formally verified code to capture floating point numbers?"
Why does it need to be floating point surely fixed point would do in this case? Its not like you need a huge range or to have high precision. The more limited the input string is the better, an input string in decimal fixed point with a limited range and precision is all you need whether you then calculate the values using fixed or floating point and binary or decimal. Furthermore sensible error handling messages and range checks/confirmations within that limited range for excessive or unusual values would be desirable.
"This is a safety critical application. Running this on an android device is a bit like trusting a chatgpt brain surgery robot to remove a brainstem tumour."
Whilst android is overkill if it is a mobile app you run on your phone it's also one less device to carry. Furthermore you can then typically provide a better UI with better history and better error/confirmation messages.
Diabetes devices have really come a long way , we have insulin pumps, finger prick glucose monitors,continuous/flash glucose monitors that go on your skin and pierce the interstitial layer of your skin and last for upto 14 days or are implantable and last longer. When you combine the two you get an artificial pancreas system like ÀPS or openAPS.