Not logged in
Log in now
Create an account
Subscribe to LWN
An unexpected perf feature
LWN.net Weekly Edition for May 16, 2013
A look at the PyPy 2.0 release
PostgreSQL 9.3 beta: Federated databases and more
LWN.net Weekly Edition for May 9, 2013
Such a statement requires omniscience.
I am afraid you are not omniscient
http://en.wikipedia.org/wiki/Polyspace (just a random example)
What every C Programmer should know about undefined behavior #2/3
Posted May 17, 2011 22:38 UTC (Tue) by cmccabe (guest, #60281)
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.
Posted May 18, 2011 0:34 UTC (Wed) by price (subscriber, #59790)
> 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.
Posted May 18, 2011 4:08 UTC (Wed) by cmccabe (guest, #60281)
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.
Posted May 18, 2011 5:02 UTC (Wed) by price (subscriber, #59790)
Definitely beats Tang, if you ask me.
Posted May 19, 2011 3:53 UTC (Thu) by raven667 (subscriber, #5198)
Posted May 19, 2011 13:11 UTC (Thu) by marcH (subscriber, #57642)
Posted May 19, 2011 18:01 UTC (Thu) by raven667 (subscriber, #5198)
Copyright © 2013, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds