> Do we, really?
Yes, or pretty close to it. What we don't know how to do (AFAIK) is do it at a cost that would be acceptable for most software. So yes, it mostly gets done for (components of) planes, spacecraft, medical devices, etc.
Totally agreed that most software is a morass of bugs. But giving examples of buggy software doesn't provide any information about whether we know how to make non-buggy software. It only provides information about whether we know how to make buggy software—spoiler alert: we do :)
> So yes, it mostly gets done for (components of) planes, spacecraft, medical devices, etc.
I have to disagree here. All of these you mentioned have regularly bugs. Multiple spacecraft got lost because of these. For planes there's not so distant Boeing 737 MAX fiasco (admittedly this was bad software behavior caused by sensor failure). And medical devices, the news about their bugs semi-regularly pop up. So while the software for these might do a bit better than the rest, they certainly are not anywhere close to being bug free.
And same goes for specifications the software is based on. Those aren't bug-free either. And writing software based on flawed specification will inevitably result in flawed software.
That's not to say we should give up on trying to write bug free software. But we currently don't know how to do so.
That software also often has bugs. It's usually a bit more likely that they are documented, though, and unlikely to cause a significant failure on their own.
> But giving examples of buggy software doesn't provide any information about whether we know how to make non-buggy software. It only provides information about whether we know how to make buggy software—spoiler alert: we do :)
Conversely, and perhaps MUCH more importantly, only saying that we know how to write relatively bug-free software without giving any evidence or proof that it is indeed the case is a gigantic red flag.
In fact, given how our brains work and how illogical we actually are, it’s quite unbelievable that we actually have the capacity to write “bug-free” code. Such a thing is much more likely to really be just a myth more than anything else, and simply saying “nuh-uh” won’t change that.
There is a huge wetware problem too. Like if I can send you an email or other message that tricks you and gets you to send me $10k, what do I care if the industry is 100% effective at blocking RCE?