| |||||||||||||
What every C Programmer should know about undefined behavior #2/3What every C Programmer should know about undefined behavior #2/3Posted May 17, 2011 22:38 UTC (Tue) by cmccabe (guest, #60281)In reply to: What every C Programmer should know about undefined behavior #2/3 by marcH Parent article: What every C Programmer should know about undefined behavior #2/3
I'm not against the use of little proof checkers when writing code. Arguably, static type systems are just examples of little proof checkers. Another example is the lexing and parsing step where the compiler decides whether your program is syntactically correct. You can argue that while parsing the program, it proves that the program is parsable.
Polyspace looks like another such tool. It can prove that certain programs clearly violate C semantics, like dereferencing a NULL pointer. But it can't prove the program as a whole correct because it doesn't have enough information about the requirements and the environment.
There are other examples of little model checkers. Sparse allows kernel hackers to annotate functions with interesting properties like what locks it takes, etc. cpplint finds potential errors in C++ programs. And -Wall and -Wextra add even more checks. Those things are great and we should have more of them.
But if you did a survey of most academic programming language departments, you would find that most of them focus on developing completely new programming languages and rewriting things from scratch. Nothing is more common than a grad student inventing a new functional programming language for his thesis. Nothing is more uncommon than an actual useful tool coming out of it. Even your own example confirms this: Polyspace is commercial and not developed in academia.
(Log in to post comments)
What every C Programmer should know about undefined behavior #2/3 Posted May 18, 2011 0:34 UTC (Wed) by price (subscriber, #59790) [Link] > Polyspace is commercial and not developed in academia. Wrong. It is commercial, but it came from academia. Quick history of Polyspace, unfortunately quoting an obituary (http://christele.faure.pagesperso-orange.fr/AlainDeutsch.html - see original for many links):
So the tool was developed by a PhD researcher working at a research lab (and well-known hotbed of static type systems), refined for several years, and finally commercialized by him and others. Another static analysis tool widely used in practice is Coverity -- that one came from a bunch of academics at Stanford. That's the usual story for this kind of tool.
What every C Programmer should know about undefined behavior #2/3 Posted May 18, 2011 4:08 UTC (Wed) by cmccabe (guest, #60281) [Link]
I stand corrected. It looks like Polyspace came mostly from academia.
It's also interesting that it was associated with the launch of a European rocket, Ariane 5. Everyone knows that the space race in the 1960s helped to push technology ahead in the United States; I guess that still happens, at least to a certain extent.
I think this kind of research is really interesting. It seems like it could help create more efficient compilers and perhaps better tools.
For what it's worth, I like static type systems. I really hope that in the future, we'll be able to have more and more information about programs even before running them. Programmers ought to be free from the drudgery of spotting typos or passing the wrong arguments to functions. Or even accidentally dereferencing a pointer before assigning it. As I said before, though, there are always things in the design that are impossible to "prove" (in the mathematical sense), like user interface, the performance of heuristic algorithms, and artistic design.
What every C Programmer should know about undefined behavior #2/3 Posted May 18, 2011 5:02 UTC (Wed) by price (subscriber, #59790) [Link]
Huh, nice observation re: this technology being connected to the space race. I hadn't made that connection.
Definitely beats Tang, if you ask me.
What every C Programmer should know about undefined behavior #2/3 Posted May 19, 2011 3:53 UTC (Thu) by raven667 (subscriber, #5198) [Link]
If Feynman is to be believed then a significant part of modern technological living was developed at least in part as part of the space race and this is evidence that this continues to be true at a smaller scale.
What every C Programmer should know about undefined behavior #2/3 Posted May 19, 2011 13:11 UTC (Thu) by marcH (subscriber, #57642) [Link]
Do not forget World War II just before that. In some cases the same people involved http://en.wikipedia.org/wiki/Wernher_von_Braun
What every C Programmer should know about undefined behavior #2/3 Posted May 19, 2011 18:01 UTC (Thu) by raven667 (subscriber, #5198) [Link]
well that part of the space race was about who captured the better germans at the end.
|
|||||||||||||