3 ms·

IMHO, more work should be done on proving properties of programs. If one could make a programming language like Dafny [1] less quirky but more developer-friendl

IMHO, more work should be done on proving properties of programs. If one could make a programming language like Dafny [1] less quirky but more developer-friendly, you can have programs which are both good-performing and proven to be consistent with their specification (but again, quirks in the specification may cause troubles).

mannykannot 9y ago
Thanks for bringing Dafny to my attention. I agree with your first sentence, which is why I think it is a big deal that it can be a great deal harder, in practice, to reason about the behavior of a C program, if optimized, than the same program un-optimized. For one thing, unless you successfully reason about what the optimized code does when deploying an optimized build, then you are not deploying the program that you analyzed or inspected. I think there is a sort of analogy with a large black hole here [1]: you can slip across the "event horizon" into undefined behavior without noticing, but, especially if you are using an optimizing compiler, there may be no escape. [1] Maybe not, if the black-hole firewall hypothesis is correct.
bluejekyll 9y ago
I'm totally unfamiliar with Dafny, the front page didn't do much more than specicify the goals. Any chance you could briefly compare it to Rust or another systems level language trying to remove undefined behavior?
- nickpsecurity 9y ago
  It's more like SPARK Ada. It's a limited language designed for easy analysis by an automated prover. You can do preconditions, postconditions, and invariants in it. It was used in ExpressOS for mobile and I think IronClad Apps, too.
  - bluejekyll 9y ago
    Are those pre and post conditions always executed? Or are they optional assertions that can be enabled/disabled?
    - neilparikh 9y ago
      If I'm reading the description correctly, the pre and post conditions are analyzed statically during compiling, and not added to the output code. So it's a similar idea to type checking, where the program won't even compile until the versifier is sure your code meets the conditions.

mannykannot 9y ago

Thanks for bringing Dafny to my attention. I agree with your first sentence, which is why I think it is a big deal that it can be a great deal harder, in practice, to reason about the behavior of a C program, if optimized, than the same program un-optimized. For one thing, unless you successfully reason about what the optimized code does when deploying an optimized build, then you are not deploying the program that you analyzed or inspected. I think there is a sort of analogy with a large black hole here [1]: you can slip across the "event horizon" into undefined behavior without noticing, but, especially if you are using an optimizing compiler, there may be no escape. [1] Maybe not, if the black-hole firewall hypothesis is correct.

bluejekyll 9y ago

I'm totally unfamiliar with Dafny, the front page didn't do much more than specicify the goals. Any chance you could briefly compare it to Rust or another systems level language trying to remove undefined behavior?

nickpsecurity 9y ago
It's more like SPARK Ada. It's a limited language designed for easy analysis by an automated prover. You can do preconditions, postconditions, and invariants in it. It was used in ExpressOS for mobile and I think IronClad Apps, too.
- bluejekyll 9y ago
  Are those pre and post conditions always executed? Or are they optional assertions that can be enabled/disabled?
  - neilparikh 9y ago
    If I'm reading the description correctly, the pre and post conditions are analyzed statically during compiling, and not added to the output code. So it's a similar idea to type checking, where the program won't even compile until the versifier is sure your code meets the conditions.