3 ms·

> No software can be quaranteed to be bug-free. Sure, this is done all the time via verification and other formal methods. It's not common in the industry, but

> No software can be quaranteed to be bug-free. Sure, this is done all the time via verification and other formal methods. It's not common in the industry, but not entirely uncommon either.

ranger_danger 4y ago
got any examples of this being used in popular FOSS software?
- naasking 4y ago
  Depends what you mean by "popular". seL4 [1] is formally verified, open source and is used as baseband firmware in millions of phones, among other uses. Google just recently started an embedded OS based on it as well. CompCert [2] is a formally verified optimizing C compiler. Most formal verification happens in compilers or low-level mission critical systems due to the cost. If you want to write some formally verified C, you can check out Frama-C [3]. [1] https://sel4.systems/ https://sel4.systems/ [2] https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert [3] https://frama-c.com/ https://frama-c.com/
  - ranger_danger 4y ago
    >all the time >not common >the cost That's what I thought... and seL4 was the only one I could think of as well. I always see arguments around auditing as well but I think realistically unless a project has some enormous resources capable of funding this things themselves, you can't expect it to happen, but so many people poo-poo projects simply because it's "not audited", but to me that's silly because 1. most projects can't afford that, 2. who gets to say what has been audited "well enough", and 3. auditing results are only valid for specific snapshots of a repo and are completely invalidated as soon as any new changes are made.
    - naasking 4y ago
      It does happen all the time in commercial contexts in certain industries. Look up Spark Ada for lots of commercials applications.
mh7 4y ago
Nope, not even formal proofs can save you, see WPA2/KRACK. Using proofs just shifts the bugs into the assumptions/axioms (i.e you think your proof is proving X but it's actually proving Y)

> No software can be quaranteed to be bug-free. Sure, this is done all the time via verification and other formal methods. It's not common in the industry, but not entirely uncommon either.

ranger_danger 4y ago

got any examples of this being used in popular FOSS software?

naasking 4y ago
Depends what you mean by "popular". seL4 [1] is formally verified, open source and is used as baseband firmware in millions of phones, among other uses. Google just recently started an embedded OS based on it as well. CompCert [2] is a formally verified optimizing C compiler. Most formal verification happens in compilers or low-level mission critical systems due to the cost. If you want to write some formally verified C, you can check out Frama-C [3]. [1] https://sel4.systems/ https://sel4.systems/ [2] https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert [3] https://frama-c.com/ https://frama-c.com/
- ranger_danger 4y ago
  >all the time >not common >the cost That's what I thought... and seL4 was the only one I could think of as well. I always see arguments around auditing as well but I think realistically unless a project has some enormous resources capable of funding this things themselves, you can't expect it to happen, but so many people poo-poo projects simply because it's "not audited", but to me that's silly because 1. most projects can't afford that, 2. who gets to say what has been audited "well enough", and 3. auditing results are only valid for specific snapshots of a repo and are completely invalidated as soon as any new changes are made.
  - naasking 4y ago
    It does happen all the time in commercial contexts in certain industries. Look up Spark Ada for lots of commercials applications.

mh7 4y ago

Nope, not even formal proofs can save you, see WPA2/KRACK. Using proofs just shifts the bugs into the assumptions/axioms (i.e you think your proof is proving X but it's actually proving Y)