5 ms·

Question unrelated to the stupidity of supporting telnet as protocol on these devices- Did you guys use formal verification techniques? http://en.wikipedia.org/

Question unrelated to the stupidity of supporting telnet as protocol on these devices- Did you guys use formal verification techniques? http://en.wikipedia.org/wiki/Formal_verification http://en.wikipedia.org/wiki/Formal_verification

voidlogic 11y ago
If some one would explain the down-voting to me, I'd love to understand... honestly 1. My question was unrelated to the poor decision the OPs former employer made to use telnet. 2. Formal verification the the gold standard in correctness often used for can't fail things like missiles and satellites.
- sfeng 11y ago
  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.
  - TazeTSchnitzel 11y ago
    "Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth
- dfc 11y ago
  There are no hard rules but this seems a little gratuitous: "Question unrelated to the stupidity of supporting telnet as protocol on these devices"
- toyg 11y ago
  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.
  - voidlogic 11y ago
    >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.
    - toyg 11y ago
      > 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 :)
- pascal_cuoq 11y ago
  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.]
  - voidlogic 11y ago
    I have heard about this from two sources: 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
jwiley 11y ago
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.
- voidlogic 11y ago
  >Formal verification would not help if the formal or informal design specs called for unauthenticated telnet This is why I qualified by question saying such.

voidlogic 11y ago

If some one would explain the down-voting to me, I'd love to understand... honestly 1. My question was unrelated to the poor decision the OPs former employer made to use telnet. 2. Formal verification the the gold standard in correctness often used for can't fail things like missiles and satellites.

sfeng 11y ago
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.
- TazeTSchnitzel 11y ago
  "Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth
dfc 11y ago
There are no hard rules but this seems a little gratuitous: "Question unrelated to the stupidity of supporting telnet as protocol on these devices"
toyg 11y ago
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.
- voidlogic 11y ago
  >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.
  - toyg 11y ago
    > 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 :)
pascal_cuoq 11y ago
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.]
- voidlogic 11y ago
  I have heard about this from two sources: 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

jwiley 11y ago

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.

voidlogic 11y ago
>Formal verification would not help if the formal or informal design specs called for unauthenticated telnet This is why I qualified by question saying such.