Formal verification would not help if the formal or informal design specs called for unauthenticated telnet. It would prove that the entire stack was bullet-proof against memory violations and mathematically pure, and that it would with 100% certainty allow untrusted users to access administrative functions.
Probably your tone. Half your post is you telling them they're stupid, and the other half is a patronizing link to very well-known concepts (implying they'd be stupid not to use them, except there are reasons why very few people actually do). It can read like the average know-it-all post plus gratuitous insults.
>Half your post is you telling them they're stupid
No I was saying my question was unrelated to a stupid decision their former employer made....
>and the other half is a patronizing link to very well-known concepts
The link was NOT for the benefit of the OP to whom I was asking a question, it was for reader here that might not know what I was referring too in the question.
> I was saying my question was unrelated to a stupid decision their former employer made
"Former employers" don't usually make decisions in a vacuum -- chances are that engineers were involved at some point, and if it wasn't OP maybe it was a colleague or even a friend. Engineers are as lazy as anyone else, and telnet is an easy protocol to support. Also "let's not talk about my opinion of X" is just a passive-aggressive way of stating your opinion without accepting a possible critique of it, which in itself is off-putting. If you really didn't want to talk about the subject, you wouldn't have mentioned it right away. The only safe use of "let's not talk about X" is as a way to move on after a topic has been discussed and agreement could not be reached.
> The link was NOT for the benefit of the OP to whom I was asking a question, it was for reader
that might as well be, but 1) both OP and HN readers will likely be familiar with the concept and/or can google it themselves, and 2) playing to the peanut gallery is patronizing in itself.
Note I'm not criticizing your positions, I'm just describing how your tone might come across as patronizing. And that's more than enough meta for a week, I think :)
If I had to guess I would say it relates to the opinion of some engineers that formal verification is only possible in relatively simple systems, and even then only as a mathematical curiosity. As true or not as that may be, the current 'collective wisdom' is more oriented towards automated testing than formal verification, and anything contrary to the popular view gets some natural resistance.
If you have references showing that formal methods are used for missiles and satellites, I would love to see them. [I work on formal methods tools and I am currently working on a usecase from the space industry, but that one is not documented yet.]
1. Papers/case studies the master's of software engineering directory at my university provided while I was in grad. I can try to dig up some of these later if you are interested.
2. Friends who either worked on satellites or airpcraft
