Does it correctly handle every possible sequence of inputs? For the vast majority of software in use today, the answer is "no"; The follow up question is "does it matter?" and (luckily or unluckily) the answer for the vast majority of software in the vast majority of use cases, is "no" as well.
But occasionally it does, e.g. https://en.wikipedia.org/wiki/Therac-25 is a famous poster child, and I quote:
>>> The failure occurred only when a particular nonstandard sequence of keystrokes was entered on the VT-100 terminal which controlled the PDP-11 computer: an "X" to (erroneously) select 25 MeV photon mode followed by "cursor up", "E" to (correctly) select 25 MeV Electron mode, then "Enter", all within eight seconds
Software was not obviously correct or incorrect; In fact, it had been acceptable for an earlier model (which had some hardware protections missing from the newer one). Reaching the incorrect state required the race described above to trigger, which did, in fact, happen in practice a handful of times.
You can work very hard to formally prove your implementation, only to find out that the compiler had a bug and makes your software bad. Or the CPU does; Or all the designs are fine, but there's an bit flip due to electro-migration or cosmic rays. Many people consider this "force majeur" - "an act of god" one cannot anticipate, but cosmic rays are in fact an expected -- and hard to avoid -- input to many systems.
You are in control of a logical model which you can, with extra work, do (provably) correctly. But that IS, from experiencce, 10x to 100x more expensive, and unless you go for 10x-100x more expensive hardware, reduces and moves the sloppiness factor around, but does not eliminate it.
I think in that light, most modern software can be built to be robust and easily maintainable rather than correct. Like the difference between building a bridge, where you understand everything in the system, versus building a vehicle engine, where you have multiple dependencies but you still need it to not catastrophically fail should any of them stop being correct (eg: fuel pump fails, engine management detects lower fuel pressure and cuts ignition, saving the engine).
I don't know a single piece of software on my computer right now that doesn't crash, act weird, hang or do something else to annoy me on a daily basis.
Now yes, each infraction might be just a minor niggle, but god it adds up!
By the end of the day, all the bugs that on their own shouldn't be too bad, leave me frustrated as hell and wanting to say fuck everyone and just go live in the woods.
It's especially worse when I know this shit doesn't need to happen.
It's all about tradeoffs. Everybody wants cheap software that works perfectly, but reality dictates that can't happen. Most of the time, cheap/free with minor annoyances is better than perfect but high-cost.
We should be worried about poor development practices in the automotive industry specifically. Looks like many manufacturers approach the tasks the same way any other hardware manufacturer does, i.e. software is secondary in their minds. Software for a car is kind of the same as software for your next "smart fridge". Among other things, it can be outsourced for example.
Whereas, as Bruce Schneier put it, a modern car is a computer on wheels, not the other way around. A computer on wheels is a lot more dangerous (and there are security implications too, it's what Schneier meant actually).
For most applications, is it worth spending several times more time and resources in order to make it "correct"? I don't think so.