6 ms·

> the borrow checker in Rust, which is a form of static analysis, is so valuable > Compare linters and style checkers Odd comparison: static analysis is way m

by nimmer 6y ago

> the borrow checker in Rust, which is a form of static analysis, is so valuable > Compare linters and style checkers Odd comparison: static analysis is way more powerful than these two examples. It can spot plenty of subtle bugs due to incorrect reasoning around a problem.

Cyph0n 6y ago
Genuinely curious: is static analysis really more powerful than the Rust type system + borrow checker? A more concrete example: is Coverity + C more powerful than Rust?
- thechao 6y ago
  There’s no model more powerful than static analysis if, by static analysis, they mean abstract interpretation: the Galois connection guarantees this.
  - throwgeorge 6y ago
    >Galois connection Lol man I've seen some funny things pulled out people's butts to sound smart but this takes the cake. Please do tell what is the connection between galois groups and static analysis.
  - littlestymaar 6y ago
    Static analysis is more than just abstract interpretation, and the OP doesn't discuss abstract interpretation at all, but talks about a design by contract approach inspired by Ada/SPARK.
    - anentropic 6y ago
      Maybe not directly mentioned in the article, but I think abstract interpretation is happening... It's talking about DrNim, and docs page for that https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html says: "DrNim combines the Nim frontend with the Z3 proof engine in order to allow verify / validate software written in Nim" So I think the design-by-contract annotations are being checked via abstract interpretation (that's what gets fed into Z3 I think?)
      - littlestymaar 6y ago
        Z3 is a contraint solver (SMT, SAT) which makes total sense to use in a design by contract system, but AFAIK there is zero link to abstract interpretation (which from what I understood about it, is way harder to use).
        anentropic 6y ago
        How else are you going to check the contracts at compile time? I honestly don't know if that's how DrNim works or if there are other ways to achieve that. But a similar tool for Python does it exactly this way: https://github.com/pschanely/CrossHair https://github.com/pschanely/CrossHair "CrossHair works by repeatedly calling your functions with symbolic inputs. It uses an SMT solver (a kind of theorem prover) to explore viable execution paths and find counterexamples for you." ...so that's where I got the idea that DrNim is probably doing the same
  - a1369209993 6y ago
    > abstract interpretation That's not what static analysis (which includes things like type-checking) means and that's not something you can do with general-purpose code, for reasons related to Rice's theorem.
    - thechao 6y ago
      Type-checking is one of the classical examples of abstract interpretation — it's mentioned in the original Cousot & Cousot paper (1977). Maybe you're thinking of something else?
- nimmer 6y ago
  > is static analysis really more powerful than the Rust type system + borrow checker? Yes, and by far. A theorem prover, as the name suggests, can be used to prove algorithmic correctness of your code.

by nimmer 6y ago

Cyph0n 6y ago

Genuinely curious: is static analysis really more powerful than the Rust type system + borrow checker? A more concrete example: is Coverity + C more powerful than Rust?

thechao 6y ago
There’s no model more powerful than static analysis if, by static analysis, they mean abstract interpretation: the Galois connection guarantees this.
- throwgeorge 6y ago
  >Galois connection Lol man I've seen some funny things pulled out people's butts to sound smart but this takes the cake. Please do tell what is the connection between galois groups and static analysis.
- littlestymaar 6y ago
  Static analysis is more than just abstract interpretation, and the OP doesn't discuss abstract interpretation at all, but talks about a design by contract approach inspired by Ada/SPARK.
  - anentropic 6y ago
    Maybe not directly mentioned in the article, but I think abstract interpretation is happening... It's talking about DrNim, and docs page for that https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html says: "DrNim combines the Nim frontend with the Z3 proof engine in order to allow verify / validate software written in Nim" So I think the design-by-contract annotations are being checked via abstract interpretation (that's what gets fed into Z3 I think?)
    - littlestymaar 6y ago
      Z3 is a contraint solver (SMT, SAT) which makes total sense to use in a design by contract system, but AFAIK there is zero link to abstract interpretation (which from what I understood about it, is way harder to use).
      - anentropic 6y ago
        How else are you going to check the contracts at compile time? I honestly don't know if that's how DrNim works or if there are other ways to achieve that. But a similar tool for Python does it exactly this way: https://github.com/pschanely/CrossHair https://github.com/pschanely/CrossHair "CrossHair works by repeatedly calling your functions with symbolic inputs. It uses an SMT solver (a kind of theorem prover) to explore viable execution paths and find counterexamples for you." ...so that's where I got the idea that DrNim is probably doing the same
- a1369209993 6y ago
  > abstract interpretation That's not what static analysis (which includes things like type-checking) means and that's not something you can do with general-purpose code, for reasons related to Rice's theorem.
  - thechao 6y ago
    Type-checking is one of the classical examples of abstract interpretation — it's mentioned in the original Cousot & Cousot paper (1977). Maybe you're thinking of something else?
nimmer 6y ago
> is static analysis really more powerful than the Rust type system + borrow checker? Yes, and by far. A theorem prover, as the name suggests, can be used to prove algorithmic correctness of your code.