5 ms·

Linux will probably get some Rust parsers in the future, which are IMHO even better because they are easy to write so you're sure they are robust - whereas form

Linux will probably get some Rust parsers in the future, which are IMHO even better because they are easy to write so you're sure they are robust - whereas formally verifying a parser may or may not be done depending on the coder's available time and willingness to do so.

UncleEntity 4y ago
If I understand this property it takes a specification and generates a formally proven parser that lets you cast the bytes to a struct or runs code to do something with the data. All automagic, can’t see how it could get much simpler than that.
deterministic 4y ago
Rust doesn’t stop you from writing buggy code. However I do agree that it is easier to write memory safe code in Rust compared with C/C++.
- masklinn 4y ago
  TBF lots of formal tools don’t either, because you still have to translate the proven code by hand. It looks like Microsoft’s does the translation, so the only risk is bugs in the code generator, which seems nice. There’s also Google’s wuffs, but I don’t think that is formal, it just ensures memory safety.
  - jnash 4y ago
    Yep if the translation is done by hand then that might be a potential problem. However a lot of modern proof tools have proven correct translators (based on the CompCert work).
- staticassertion 4y ago
  No amount of formal verification stops you from writing buggy code.
  - jnash 4y ago
    I don't think you understand what "proven correct" means. If you formally prove a spec correct using modern proof tools then it is guaranteed to have zero bugs. Nobody has found even a single bug in the proven correct CompCert C compiler for example. However people find bugs in gcc all the time.
    - staticassertion 4y ago
      It means that a program has been verified against a model, and properties of that model are held true. What it does not mean is that the program is bug free. That would, of course, violate the halting problem, or its generalization Rice's Theorem - non-trivial programs can not have arbitrary properties proven about them. There's also Gödel's Incompleteness Theorem, obviously, as well as the fact that a proof is only as good as its model.
      - UncleMeat 4y ago
        It wouldn’t break Rice’s Thm to prove it for a particular program. All Rice’s Thm says is that any algorithm must fail on some programs.
        staticassertion 4y ago
        It would if you're talking about arbitrary classes of bugs.
        UncleMeat 4y ago
        Not so. Consider the algorithm that reports "Yes" for all inputs for all program properties. For a large number of programs and properties, this algorithm will report the correct information.
      - mbrodersen 4y ago
        Not true for non-Turing complete languages. Which is why all proof tools require a proof of termination. Some do it automatically (essential ruling out Turing complete languages) others require a formal proof of termination by the user.
HillBates 4y ago
formal verification is about functionality, not about your emotions.
- zen_1 4y ago
  Haven't you heard? The only bugs are those caused by memory safety, and only switching to Rust can save us from the insanity of managing our own memory.
  - jnash 4y ago
    You are joking right? Just checking :)
    - zen_1 4y ago
      Yes, I was being quite sarcastic above
0x69420 4y ago
f* (one system on display in this paper) can extract to c/assembler suitable for inclusion in a hand-written c source tree, all the while giving a wider and more interesting set of guarantees with the added benefit that you won't have to depend on a rust toolchain to build your project (bootstrapping f* is considerably easier, and you only have to do it when you check in your verified bits) funny enough, much like rust, one of its most widely-deployed applications lives in firefox; see project-everest.github.io

UncleEntity 4y ago

If I understand this property it takes a specification and generates a formally proven parser that lets you cast the bytes to a struct or runs code to do something with the data. All automagic, can’t see how it could get much simpler than that.

deterministic 4y ago

Rust doesn’t stop you from writing buggy code. However I do agree that it is easier to write memory safe code in Rust compared with C/C++.

masklinn 4y ago
TBF lots of formal tools don’t either, because you still have to translate the proven code by hand. It looks like Microsoft’s does the translation, so the only risk is bugs in the code generator, which seems nice. There’s also Google’s wuffs, but I don’t think that is formal, it just ensures memory safety.
- jnash 4y ago
  Yep if the translation is done by hand then that might be a potential problem. However a lot of modern proof tools have proven correct translators (based on the CompCert work).
staticassertion 4y ago
No amount of formal verification stops you from writing buggy code.
- jnash 4y ago
  I don't think you understand what "proven correct" means. If you formally prove a spec correct using modern proof tools then it is guaranteed to have zero bugs. Nobody has found even a single bug in the proven correct CompCert C compiler for example. However people find bugs in gcc all the time.
  - staticassertion 4y ago
    It means that a program has been verified against a model, and properties of that model are held true. What it does not mean is that the program is bug free. That would, of course, violate the halting problem, or its generalization Rice's Theorem - non-trivial programs can not have arbitrary properties proven about them. There's also Gödel's Incompleteness Theorem, obviously, as well as the fact that a proof is only as good as its model.
    - UncleMeat 4y ago
      It wouldn’t break Rice’s Thm to prove it for a particular program. All Rice’s Thm says is that any algorithm must fail on some programs.
      - staticassertion 4y ago
        It would if you're talking about arbitrary classes of bugs.
        UncleMeat 4y ago
        Not so. Consider the algorithm that reports "Yes" for all inputs for all program properties. For a large number of programs and properties, this algorithm will report the correct information.
    - mbrodersen 4y ago
      Not true for non-Turing complete languages. Which is why all proof tools require a proof of termination. Some do it automatically (essential ruling out Turing complete languages) others require a formal proof of termination by the user.

HillBates 4y ago

formal verification is about functionality, not about your emotions.

zen_1 4y ago
Haven't you heard? The only bugs are those caused by memory safety, and only switching to Rust can save us from the insanity of managing our own memory.
- jnash 4y ago
  You are joking right? Just checking :)
  - zen_1 4y ago
    Yes, I was being quite sarcastic above

0x69420 4y ago

f* (one system on display in this paper) can extract to c/assembler suitable for inclusion in a hand-written c source tree, all the while giving a wider and more interesting set of guarantees with the added benefit that you won't have to depend on a rust toolchain to build your project (bootstrapping f* is considerably easier, and you only have to do it when you check in your verified bits) funny enough, much like rust, one of its most widely-deployed applications lives in firefox; see project-everest.github.io