4 ms·

> Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm

> Unless you can point out a static code analyzer which performs the sort of check that complies with your personal beliefs, it will remain firmly in the realm of practical impossibility. Here's a list: https://en.wikipedia.org/wiki/Symbolic_execution#Tools https://en.wikipedia.org/wiki/Symbolic_execution#Tools Also related: https://en.wikipedia.org/wiki/Abstract_interpretation https://en.wikipedia.org/wiki/Abstract_interpretation > C is now what? 5 decades old? Wouldn't that be enough time for anyone to roll that out if it was in fact feasible? Depends on how you define "feasible". Abstract interpretation and symbolic execution are crazy complex¹. Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types. Trying to make static guaranties about imperative code is indeed a dead end by now. The problem is that proving any properties of imperative code needs much more effort (and therefore code) than what is expressed by the code that needs proves, so it's actually likely that you haven than bugs in the code that proves things. So this approach is not really "feasible" in the end. --- ¹ Just have a look at the documentation around the KeY tool used to prove things about Java programs. https://www.key-project.org/thebook2/ https://www.key-project.org/thebook2/ That's the most complex stuff I've ever seen! Depended type systems are "trivially simple" in contrast, no joke. But this is just about a "simple language" like Java… The complexity of C is much much higher.

zozbot234 4y ago
Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking.
- still_grokking 4y ago
  > Type checking is actually a special case of abstract interpretation. I'm not sure about that. Maybe in regard to type level functions? But else? I'm skeptical. Could you explain what you exactly mean? Preferably with some examples as I'm having a hard time to imagine something in that direction. > For all we know, it may even be that dependent types can already express many complex uses of it; That for sure! Otherwise, corresponding type systems wouldn't be considered being an alternative. Depended types can express anything computable. (Which also makes them undecidable in general). In theory, you can prove any property of a program using depended types. That's why they're the preferred method by now. But you can't bold on such thing after the fact usually. Your language needs to be pure to benefit form the proving powers of depended types. So no hope for C and such like.
  - ryao 4y ago
    He appears to be right in saying "Type checking is actually a special case of abstract interpretation". The paper that presented Abstract Interpretation to the world concludes: "It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..." https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf https://www.di.ens.fr/~cousot/publications.www/CousotCousot-... That said, abstract interpretation promises that the absence of reports proves the absence of the errors that the sound static analyzer implementing it is designed to catch. Provided that you do not abuse casts/unions, the absence of warnings/errors from a compiler's type checking on a strongly typed language should prove an absence of type errors, which does sound like what abstract interpretation promises. Lastly, I need make time to actually read that paper. I have only read a very small part of it.
  - zozbot234 4y ago
    You could model C in a dependently-typed language by embedding the C abstract machine and C program expressions in it. Then you could use the Poincaré principle applied to C-program fragments to perform any "abstract interpretation" of them and derive any property you might care about. So it looks like the Poincaré's principle (as it was named by Barendegt) is the actual "missing link" that would enable you to generalize from purely syntax-based analysis (as in the traditional definition of type systems/type checks) to "interpretation" of a more general sort.
- ryao 4y ago
  > Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking. See the paper that presented abstract interpretation to the world: "It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..." https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf https://www.di.ens.fr/~cousot/publications.www/CousotCousot-...
ryao 4y ago
> Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types. This is not entirely true. Patrick Cousot‘s group, which invented the theory of abstract interpretation, kept working on it and produced Astree. I had previously been under the impression that Astree was from the same people that made Compcert C, but upon double checking for this reply, I realized that was wrong. The two groups are both in France though. It was an easy mistake to make considering that Absint sells licenses for both. > Trying to make static guaranties about imperative code is indeed a dead end by now. The astree static analyzer is available from Absint. One of the inventors of both it and the theory on which it is based is also still alive: https://en.wikipedia.org/wiki/Patrick_Cousot https://en.wikipedia.org/wiki/Patrick_Cousot His software is in use at the ESA and other places. NASA is using software it wrote in house based on that theory: https://www.nasa.gov/aero/ikos.html https://www.nasa.gov/aero/ikos.html Presumably, NASA heard about Astree from the ESA and decided to make its own tool, possibly due to NIH syndrome. I am not sure if NASA counts as academia. This is far from a dead end, even if most researchers cannot be bothered to do things in that area. You will probably find a number of the ones that can be bothered to do things in that area at farma-c: https://frama-c.com/ https://frama-c.com/
- GoblinSlayer 4y ago
  It's justified for aerospace, because failures are quite expensive there, but for usual business it will be much easier to implement automatic bound checking, like at 1% complexity of the C compiler.
  - ryao 4y ago
    I wonder what operating systems the aerospace industry uses, since failures in the operating system could be equally expensive, yet operating system developers generally do not have access to these tools.
    - camgunz 4y ago
      Much of the time they build their own.

zozbot234 4y ago

Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking.

still_grokking 4y ago
> Type checking is actually a special case of abstract interpretation. I'm not sure about that. Maybe in regard to type level functions? But else? I'm skeptical. Could you explain what you exactly mean? Preferably with some examples as I'm having a hard time to imagine something in that direction. > For all we know, it may even be that dependent types can already express many complex uses of it; That for sure! Otherwise, corresponding type systems wouldn't be considered being an alternative. Depended types can express anything computable. (Which also makes them undecidable in general). In theory, you can prove any property of a program using depended types. That's why they're the preferred method by now. But you can't bold on such thing after the fact usually. Your language needs to be pure to benefit form the proving powers of depended types. So no hope for C and such like.
- ryao 4y ago
  He appears to be right in saying "Type checking is actually a special case of abstract interpretation". The paper that presented Abstract Interpretation to the world concludes: "It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..." https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf https://www.di.ens.fr/~cousot/publications.www/CousotCousot-... That said, abstract interpretation promises that the absence of reports proves the absence of the errors that the sound static analyzer implementing it is designed to catch. Provided that you do not abuse casts/unions, the absence of warnings/errors from a compiler's type checking on a strongly typed language should prove an absence of type errors, which does sound like what abstract interpretation promises. Lastly, I need make time to actually read that paper. I have only read a very small part of it.
- zozbot234 4y ago
  You could model C in a dependently-typed language by embedding the C abstract machine and C program expressions in it. Then you could use the Poincaré principle applied to C-program fragments to perform any "abstract interpretation" of them and derive any property you might care about. So it looks like the Poincaré's principle (as it was named by Barendegt) is the actual "missing link" that would enable you to generalize from purely syntax-based analysis (as in the traditional definition of type systems/type checks) to "interpretation" of a more general sort.
ryao 4y ago
> Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking. See the paper that presented abstract interpretation to the world: "It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..." https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf https://www.di.ens.fr/~cousot/publications.www/CousotCousot-...

ryao 4y ago

> Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types. This is not entirely true. Patrick Cousot‘s group, which invented the theory of abstract interpretation, kept working on it and produced Astree. I had previously been under the impression that Astree was from the same people that made Compcert C, but upon double checking for this reply, I realized that was wrong. The two groups are both in France though. It was an easy mistake to make considering that Absint sells licenses for both. > Trying to make static guaranties about imperative code is indeed a dead end by now. The astree static analyzer is available from Absint. One of the inventors of both it and the theory on which it is based is also still alive: https://en.wikipedia.org/wiki/Patrick_Cousot https://en.wikipedia.org/wiki/Patrick_Cousot His software is in use at the ESA and other places. NASA is using software it wrote in house based on that theory: https://www.nasa.gov/aero/ikos.html https://www.nasa.gov/aero/ikos.html Presumably, NASA heard about Astree from the ESA and decided to make its own tool, possibly due to NIH syndrome. I am not sure if NASA counts as academia. This is far from a dead end, even if most researchers cannot be bothered to do things in that area. You will probably find a number of the ones that can be bothered to do things in that area at farma-c: https://frama-c.com/ https://frama-c.com/

GoblinSlayer 4y ago
It's justified for aerospace, because failures are quite expensive there, but for usual business it will be much easier to implement automatic bound checking, like at 1% complexity of the C compiler.
- ryao 4y ago
  I wonder what operating systems the aerospace industry uses, since failures in the operating system could be equally expensive, yet operating system developers generally do not have access to these tools.
  - camgunz 4y ago
    Much of the time they build their own.