Is suspect we're referring to different types of proof here. The sort of formal proof I refer to guarantees that the software will never display unspecified beh

Is suspect we're referring to different types of proof here. The sort of formal proof I refer to guarantees that the software will never display unspecified behaviour; your procedures are now backed by mathematical definitions with known properties. It's not about security. It's about the software functioning correctly so no functional updates are necessary, diminishing the need for remote updates and all the security problems that bring along. Even if remote access is needed to conveniently store various data in a different location there is no need to run everything on the same level. Smartphones are mass-produced computers that separate concerns with having a baseband and a main cpu. There is no reason a medical device could not have such a separation. One OS to keep the device working correctly under all circumstances, one OS to slap networking and interfacing on. I don't expect the medical technology industry to change quickly, but as things are they are adopting bad practices of software development and moving in the wrong direction. "If problems pop up, we'll update it later remotely" should not be an acceptable mindset for some classes of computer equipment.