4 ms·

- formally verified software I only remember hearing about "mathematically proven software" as an undergrad and just googled to find this name. I've always be

- formally verified software I only remember hearing about "mathematically proven software" as an undergrad and just googled to find this name. I've always been interested in learning more of what it's about but never jumped in.

sixstringtheory 7y ago
Check this out: https://news.ycombinator.com/item?id=22082869 https://news.ycombinator.com/item?id=22082869 How Amazon Web Services Uses Formal Methods
- gibbonsrcool 7y ago
  Thanks!
goto11 7y ago
Formal verification just proves that the software conforms to some specification. How do you proved the spec has no mistakes?
aidenn0 7y ago
Formally verified software still has its limitations. Knuth's famous "Beware of bugs in the above code; I have only proved it correct, not tried it." is funny but true. Formal verification is a good and useful tool, but it provably cannot cover the entire system, and practical limitations will limit it even further. Formal verification of source code is still subject to compiler bugs. Formally proven compilers are subject to bugs in the larger system (IIRC Csmith was able to find an incorrectness in code generated by CompCert because of a bug in a system header file).
- Gibbon1 7y ago
  Also formally verified code may behave very badly when the underlying hardware fails.
  - gpm 7y ago
    If the hardware is behaving out of spec, it's not the software failing. If the hardware is behaving in spec (e.g. 1 out of 3 computers fails) and you properly formally verified the software to that spec, the software will not behave badly.
quickthrower2 7y ago
Formally verified gets rid of a class of bugs, but you can still have a bad specification. Also what is a bug might change in the future. I imagine as we learn more from plane crashes what is ok today might be a big tomorrow.
lrem 7y ago
Think of it as writing the software in a very barebones language and then requiring unit test coverage of all possible input combinations, asserting the full output. A lot of work, but gives you reasonable certainty that your code is indeed correct (does what it was designed to do). That's at least what I learned in that one masters course. After implementing the final assignment, which was equivalent to some three lines of C and took a team of four "the semester", I've decided to not look any further into it. It is being used in applications that warrant actual investment into bug-free code, say nuclear reactor control or helicopter rotor control. I would imagine the MCAS belongs to this class. But even if your software is correct, the design it implements might be flawed, say by assuming the input you get from a single fallible sensor is to be trusted.

sixstringtheory 7y ago

Check this out: https://news.ycombinator.com/item?id=22082869 https://news.ycombinator.com/item?id=22082869 How Amazon Web Services Uses Formal Methods

gibbonsrcool 7y ago
Thanks!

goto11 7y ago

Formal verification just proves that the software conforms to some specification. How do you proved the spec has no mistakes?

aidenn0 7y ago

Formally verified software still has its limitations. Knuth's famous "Beware of bugs in the above code; I have only proved it correct, not tried it." is funny but true. Formal verification is a good and useful tool, but it provably cannot cover the entire system, and practical limitations will limit it even further. Formal verification of source code is still subject to compiler bugs. Formally proven compilers are subject to bugs in the larger system (IIRC Csmith was able to find an incorrectness in code generated by CompCert because of a bug in a system header file).

Gibbon1 7y ago
Also formally verified code may behave very badly when the underlying hardware fails.
- gpm 7y ago
  If the hardware is behaving out of spec, it's not the software failing. If the hardware is behaving in spec (e.g. 1 out of 3 computers fails) and you properly formally verified the software to that spec, the software will not behave badly.

quickthrower2 7y ago

Formally verified gets rid of a class of bugs, but you can still have a bad specification. Also what is a bug might change in the future. I imagine as we learn more from plane crashes what is ok today might be a big tomorrow.

lrem 7y ago

Think of it as writing the software in a very barebones language and then requiring unit test coverage of all possible input combinations, asserting the full output. A lot of work, but gives you reasonable certainty that your code is indeed correct (does what it was designed to do). That's at least what I learned in that one masters course. After implementing the final assignment, which was equivalent to some three lines of C and took a team of four "the semester", I've decided to not look any further into it. It is being used in applications that warrant actual investment into bug-free code, say nuclear reactor control or helicopter rotor control. I would imagine the MCAS belongs to this class. But even if your software is correct, the design it implements might be flawed, say by assuming the input you get from a single fallible sensor is to be trusted.