8 ms·

There are two kinds of software: - buggy - the one where bugs were not yet found

by sheeshkebab 7y ago

opwieurposiu 7y ago
- software with off-by-one errors
- noonespecial 7y ago
  There's a fourth one but its undefined.
  - kibwen 7y ago
    There are actually ten, but the latter six have yet to be documented.
    - dev-ns8 7y ago
      OB1 errror, sorry. Actually 9, one slots null
rosybox 7y ago
my hello world has no bugs!
- mirekrusin 7y ago
  Is it enterprise ready like this one https://gist.github.com/lolzballs/2152bc0f31ee0286b722 https://gist.github.com/lolzballs/2152bc0f31ee0286b722 ? Even that one is alpha quality, no soap support, no saml2.0, xml is not even mentioned once. It needs couple of major versions before it can reach production in express, standard, developer, enterprise and pro distributions.
- IMTDb 7y ago
  But the kernel and/or the CPU you are running it on does.
gibbonsrcool 7y ago
- 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.
    - 7y ago

There are two kinds of software: - buggy - the one where bugs were not yet found

opwieurposiu 7y ago

- software with off-by-one errors

noonespecial 7y ago
There's a fourth one but its undefined.
- kibwen 7y ago
  There are actually ten, but the latter six have yet to be documented.
  - dev-ns8 7y ago
    OB1 errror, sorry. Actually 9, one slots null

rosybox 7y ago

my hello world has no bugs!

mirekrusin 7y ago
Is it enterprise ready like this one https://gist.github.com/lolzballs/2152bc0f31ee0286b722 https://gist.github.com/lolzballs/2152bc0f31ee0286b722 ? Even that one is alpha quality, no soap support, no saml2.0, xml is not even mentioned once. It needs couple of major versions before it can reach production in express, standard, developer, enterprise and pro distributions.
IMTDb 7y ago
But the kernel and/or the CPU you are running it on does.

gibbonsrcool 7y ago

- 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.
  - 7y ago