These three quotes are logically related to each other. Have you figured out their logical connections? ;-)
UNIX is simple, it just takes a genius to understand its simplicity. —Dennis Ritchie
This suit of clothes is invisible to those unfit for their positions, stupid, or incompetent. —the emperor’s weavers
If you can’t explain it to a six year old, you don’t understand it yourself. —Albert Einstein
I have built a similar static analysis tool for Ruby. The result is a new open-source project RubySonar. RubySonar can now process the full Ruby standard library, Ruby on Rails, and Ruby apps such as Homebrew.
RubySonar’s analysis is inter-procedural and is sensitive to both data-flow and control-flow, which makes it highly accurate. RubSonar uses the same type inference technique of PySonar, and thus can resolve some of the difficult cases that can challenge a good Ruby IDE.
Dear Haskell Curry and W.A. Howard,
Like many others, I have high appreciation of the beauty in your works, but I think your discoveries about the Curry-Howard correspondence have been taken too far by the programming languages research community. Following several of your examples showing the similarity between types and logic theorems, some of the researchers started to believe that all programs are just proofs and their types the corresponding theorems. In their own words: “Types are theorems. Programs are proofs.”
I think it’s just the other way around: “Proofs are programs, but programs may not be proofs”. All proofs are programs, but only some of the programs are proofs. In mathematical terms, programs are a strict superset of proofs. Many programs are not proofs simply because proving things is not why they are made. They exist to serve other purposes. Some of them (such as operating systems) may not even terminate, thus failing the most important criteria of being a proof, but they are perfectly legitimate and important programs. Programs are more physical than math and logic—they are real things similar to flowers, trees, animals (or their excrement), cars, paintings, buildings, mountains, the earth and the sun. Their existence is beyond reason. Calling all of them proofs is a bit far-fetched in my opinion :-)
Sometimes we can derive theorems from programs and say something about their properties, but way too many times we can’t. This is the similar to the fact that sometimes we can derive math theorems from the real world but we don’t always succeed. When we fail to predict the future, we can still live it. Similarly, when math and logic fail to predict the behavior of programs, they may still run without problems. It would be nice if more programs are designed in nice ways such that we can predict how they will behave, but there is a limit as to how far we can see into their future. Thanks to this limit, because if all the future can be predicted, programs may not worth existing and life may not worth living.
Ever since I made a static analysis tool for Python called PySonar, I have been asked about the question: “What is the difference between testing and static analysis?” When I worked at Coverity, my coworkers told me that they also spent quite some time explaining to people about their difference. My answer to this question evolves as my understanding of this area deepens. Recently I replied to a comment asking a similar question, so I think it’s a good time to write down some systematic answer for this question.
Static analysis and tests are similar in their purposes. They are both tools for improving code quality. But they are very different in nature: static analysis is (of course) static, but tests are dynamic. “Static” basically means “without running the program”.
Static analysis is similar to the compiler’s type checker but usually a lot more powerful. Static analysis finds more than type errors. It can find defects such as resource leaks, array index out of bounds, security risks etc. Advanced static analysis tools may contain some capabilities of an automatic theorem prover. In essence a type checker can be considered a static analysis with a coarse precision.
Static analysis is like predicting the future, but testing is like doing small experiments in real life. Static analysis has the “reasoning power” that tests hasn’t, so static analysis can find problems that tests may never detect. For example, a security static analysis may show you how your website can be hacked after a series of events that you may never thought of.
On the other hand, tests just run the programs with certain inputs. They are fully dynamic, so you can’t test all cases but just some of them. But because tests run dynamically, they may detect bugs that static analysis can’t find. For example, tests may find that your autopilot program produces wrong results at certain altitude and speed. Static analysis tools can’t check this kind of complex dynamic properties because they don’t have access to the actual running situation.
But notice that although tests can tell you that your algorithm is wrong, they can’t tell you that it is correct. To guarantee the correctness of programs is terribly harder than tests or static analysis. You need a mechanical proof of the program’s correctness, which means at the moment that you need a theorem prover (or proof assistant) such as Coq, Isabelle or ACL2, lots of knowledge of math and logic, lots of experience dealing with those tools’ quirks, lots of time, and even with all those you may not be able to prove it, because you program can easily encode something like the Collatz conjecture in it. So the program’s passing the tests doesn’t mean it is correct. It only means that you haven’t done terribly stupid things.
Testing requires lots of manual work. Tests for “silly bugs” (such as null pointer dereference) are very boring and tedious to make. Because of the design flaws of lots of programming languages, those things can happen anywhere in the code, so you need a good coverage in order to prevent them.
You can’t just make sure that every line of the code is covered by the tests, you need good path coverage. But in the worst case, the number of execution paths of the program is exponential to its size, so it is almost impossible to get good path coverage however careful you are.
On the other hand, static analysis is fully automatic. It explores all paths in the program systematically, so you get very high path coverage for free. Because of the exponential algorithm complexity exploring the paths, static analysis tools may use some heuristics to cut down running time, so the coverage may not be 100%, but it’s still enormously higher than any human test writer can get.
Even when you get good path coverage in tests, you may still miss lots of bugs. Because you can only pass specific values into the tests, the code can still crash at the values that you haven’t tested. In comparison, static analysis processes the code symbolically. It doesn’t assume specific values for variables. It reasons about all possible values for every variable. This is a bit like computer algebra systems (e.g. Mathematica) although it doesn’t do sophisticated math.
The most powerful static analysis tools can keep track of specific ranges of the numbers that the variables represent, so they may statically detect bugs such as “array index out of bound” etc. Tests may detect those bugs too, but only if you pass them specific values that hits the boundary conditions. Those tests are painful to make, because the indexes may come after a series of arithmetic operations. You will have a hard time finding the cases where the final result can hit the boundary.
Some static analysis tools may be designed to be conservative. That is, whenever it is unsure, it can assume that the worst things can happen and issue a warning: “You may have a problem here.” Thus in principle it can tell you whenever some code may cause trouble. But a lot of times the bugs may never happen, this is called a false positive. This is like your doctor misdiagnosed you to have some disease which you don’t have. Lots of the work in building static analysis tools is about how to reduce the false positive rate, so that the users don’t lose faith in the diagnosis reports.
Tests don’t have false positives, because when they fail your program will surely fail under those conditions.
Although static analysis tools don’t have the power to guarantee the correctness of programs, they are the most powerful bug-finding tools that don’t need lots of manual labor. They can prevent lots of the silly bugs that we spend a lot of time and energy writing tests for. Some of those bugs are stupid but very easy to make. Once they happen they may crash an airplane or launch a missile. So static analysis is a very useful and valuable tool. It takes over the mindless and tedious jobs from human testers so that they can focus on more intellectual and interesting tests.
(The above picture was taken from: http://sourcegraph.com/github.com/mitsuhiko/flask)
I recently joined a newly founded company called Sourcegraph.com. We build an intelligent code search engine using some of the most powerful programming language technologies.
The difference between Sourcegraph and other code search sites is: Sourcegraph truly understands code and produces accurate results. Sourcegraph lets you semantically search and browse opensource code on the web in a similar fashion as you do locally with IDEs. It also finds users of your code worldwide, and show exactly how they use your code.
For example the following is what Sourcegraph shows you about Flask framework’s Flask.route method.
Two weeks since joining, I have successfully integrated PySonar2‘s type inference and indexing features with Sourcegraph.com, so that it can now show inferred types for Python functions. This is an advanced feature currently not available in any Python IDE.
For example, the following is the “Top Functions” page for the Flask framework, showing the PySonar2 inferred types. Notice that the parameters are not type-annotated. PySonar2 infers the types by an advanced interprocedural analysis.
You can browse your GitHub by prepending “http://sourcegraph.com/” to your GitHub repo’s address. For example, if your repo address is github.com/myname/myrepo, then you put this address into the browser:
Currently this trick works only for GitHub addresses. If Sourcegraph hasn’t yet processed the repo, it will queue it and start analyzing as soon as possible. Usually this finishes within a few minutes up to half an hour, depending on how large the repository is and how busy the servers are. Sourcegraph currently supports Go, JavaScript, Python and Ruby. More languages are under development.
All our features are still in beta and may contain quite some bugs and many areas of improvements. You are very welcome to send bug reports and feature requests to us.
In general, functional languages are pleasant to work with because they support first-class functions, which are a very powerful modeling tool. But if you pursue the extreme — to use a purely functional language, you get adverse effects similar to OO design patterns. In a conventional OO language, having to use OO design patterns makes hard things even harder; but in a purely functional language, having to use pure functions to model side-effects makes trivial things hard and hard things impossible. So speaking of the two evils, OOP is the lesser one because at least easy things are still easy in them.
The problem with pure FP is: there exists things that are not pure.
Electrical engineers probably have the best understanding of purely functional languages, because electric wires are pure by default (if you are not paranoid enough to count heat as a side-effect). Purely functional languages are the analogous of combinational logic circuits. They are very useful and are an important part of a system, but you can’t use them alone to build up complex systems. This is why people invented flip-flops and sequential logic circuits. If you look at the design of the flip-flops, you will start to appreciate the ingenuity in them. They create memory out of “pure circuits”. And the memory is where the side-effects come from.
So pureness comes for free, but side-effects took efforts to invent. Unfortunately a large portion of the physical capabilities provided by the sequential circuits are disregarded by purely functional languages. Instead, purely functional languages are obsessed in simulating the effects on their own. There is a difference between the physical and the simulated. The simulated can’t be as efficient as the physical.
For a simple example, many efficient data structures rely on mutations to create connections between their components (think about circular data structures and networks). In such structures, side-effects act very much like a physical force to hold the parts together, and update them as needed. To implement this in a purely functional language, you have to use indirect ways. Every time you change it, you need to create a new data structure which shares most of the old data structure. But then you got into the trouble of keeping track of where the “current structure” is. It is moving in the dataflow and you have to pass it on. Had you used side-effects, the structure can stay at the same location, so you won’t need to worry that you will lose track of it. You don’t need to pass it on. This will save lots of administrative code.
Also sharing the old structures induces extra levels of indirection in the data structure, which causes significant overhead. Thus purely functional data structures can’t really match the performance provided by its impure counterpart. Purely functional data structures also cause lots of object creation and thus stress the garbage collector.
Some people say that purely functional data structures will reduce contention when there is lots of concurrency, but notice that if the observers of the old data structure “purely update” it, they will hold a different structure other than it’s current state. After that point, the universe is “forked” and they will live in completely different worlds. You will lose consistency. If you really want all threads to see the same data structure, then the contention is unavoidable, because you need a channel for the information to pass through. Nothing can save you from the contention because there is data dependency.
Everything is persistent in purely functional data structures, but how often do you need the outdated ones? In impure data structures, you still have the choice of making copies when necessary and achieve the same persistence effect, just with better performance.
Purely functional languages also complicates the programs and ensue a huge cognitive cost. Modeling side-effects using pure functions is in the same mentality of wrapping functions inside objects as in OOP. They are both over-engineering and cause unnecessary manual labor.
One of the major “design patterns” in purely functional languages is called “monads”, a highly stylized way of structuring side-effects. If you look deep into them, monads make programs complicated and hard to write, and monad transformers are in essence a hack to get around monads’ limitations — they are not principled ways of composing monads. Representing side-effects using monads is as convoluted as writing interpreters or compilers using visitor patterns. For this matter, I wrote a short article some time ago which not many people have read:
To write programs in a purely functional programming language is much like living in a wired world. In such a world, there are no electromagnetic waves nor sound waves, so you don’t have wifi, cell phones, satellite TV, radios, etc. You don’t even have light or sound. In other words, everything is blind and deaf.
All information must pass through wires or pipes, connected by switch boxes which we call “monads”. You must carefully route all the wires and pipes and connect them correctly before any information processing device, including your eyes and ears, can properly work.
Trivial things in other languages (such as random number generators or circular data structures) become non-trivial in a purely functional language. Easy things often become research problems when you try to write them using monads, so you often see papers titled similar to “A Monadic Approach to a-solved-problem”.
About this I have an interesting story to tell. Once upon a time, my PhD advisor Amr Sabry tried to reimplement Dan Friedman’s miniKanren (a logic programming language) in Haskell, but he couldn’t figure out how to compose the monads. He asked for help from Oleg Kiselyov, arguably the world’s most knowledgeable person about getting around Haskell’s type system. And if you don’t know, Amr Sabry is probably the world’s most knowledgeable person about purely functional programming languages and side-effects. His paper What is a Purely Functional Language is often referred to as the official definition of “pureness”. After solving the problem with Oleg’s help, they coauthored a Functional Pearl paper. Ironically, Dan Friedman, the original author of that piece of code, didn’t have any such trouble writing it in Scheme in the first place. Certainly there is no reason Amr should be able to figure out how to compose the monads. He and Oleg just wrote the Haskell code for fun, but this story tells me something about monads: they make things unnecessarily complicated.
How did Dan Friedman write the code so easily? He just directly passed the states in-and-out and not using any monads, or you can say that he used monads’ essence without actually using them. Following Dan’s style, I rewrote miniKanren, added constraint logic programming and a highly sophisticated negation operator to it. All this is done within three weeks during my first semester as a PhD student, together with Dan’s B521, Amr’s B522, other course loads and teaching duties. I would certainly be bogged down had I used monads, and I don’t see any point of translating it into a monadic style. It is just so much simpler without monads.
(Correction to some historical facts by request from Prof. Friedman: He’d like to give a lot of the credits of the current miniKanren code’s simplicity to Chung-chieh Shan, who at one moment simplified the code to its current style.)
On the safety side, purely functional languages haven’t much advantage either. Some people claim that the value of monads is that they explicitly delimit the side-effects and support equational reasoning, but programs are not always as easy as algebra formulas such as a(b+c)=ab+a*c. If all programs are that easy, we would not need monads at all. Monads don’t really make your program easier to reason about.
Pure functions always return the same results when they are given the same input, but every monadic function has an extra “implicit” argument which is different at every call to the same function, so although it is still true that “pure functions always return the same results when they are given the same input”, the problem is, you never get the same input because of that always-changing extra argument! You don’t know what’s inside that argument. That argument is called the “state”.
There is no way you can statically know the values inside state monads, for the same reason that you don’t know the values inside the heap. This is because the state monads are in essence the same as the heap. The heap maps memory addresses to values, and state monads map variables to values. If you have written static analysis, it will be clear that monadic code is in essence putting parts of a static analysis into the user’s code. In other words, every monadic code is reimplementing part of a static analysis. So monadic code is as hard to analyze as if you use side-effects, only that it takes a lot more work to write. You can write horribly side-effective code with monads which nobody can understand and no static analysis tool can help. There is no such thing monads can make easier which can’t be done by static analysis. Static analysis researchers know this very well.
Monads are contagious. Once the code gets into monads, it is not easy to get out. Having to explicitly specify side-effects in the types is similar to having to explicitly declare exceptions in Java. You must either “handle” it, or you must declare that you have passed it on. Why should programmers write them while they can be easily inferred by static analysis? Static analysis use what is essentially monads (or even more advanced techniques), and they take the burden of writing monadic code away from programmers.
Of course overusing side-effects will make programs harder to analyze, but you can reduce side-effects and write pure functions even in an impure language. For example, the following C function is a pure function, satisfying every requirement of the definition of “pureness”.
int f(int x) {
int y = 0;
int z = 0;
y = 2 * x;
z = y + 1;
return z / 3;
}
Advanced static analysis tools would have no trouble figuring out things about this kind of code. They would know that this function is pure without you writing any annotations, and they can do a lot more for you than this. So pure functions don’t just belong to purely functional languages. You can write pure functions in any language (including assembly), but the point is, you should be allowed to use side-effects too, especially when they make things easier.
Looking back into history, the dogma from mathematics is the driving force behind purely functional languages. Mathematical functions are simple and beautiful, but unfortunately they work well only when the thing you are trying to model is pure by nature. Purely functional language proponents like using buzzwords like “category theory”, and call those who don’t understand it “uninitiated”. I know a considerable amount of category theory. Even the category theorists themselves call it “abstract nonsense”, because it is to a large extent a grotesque way of saying what other mathematicians already know, in much the same sense that GoF design patterns are a grotesque way of saying what most decent programmers already know. So category theory is the analogous of design patterns in mathematics.
If you read Gottlob Frege’s article Function and concept, you will be surprised that most mathematicians got functions wrong before his writing, and that was just a little more than a hundred years ago. Mathematics have done lots of things wrong with its language. This has been pointed out a long time ago by Gerald Susman in his Structure and Interpretation of Classical Mechanics and recently in his InfoQ talk. There is a lot of truth in his words. There is no reason programming language designers should blindly follow the ways of mathematics, because it is just another quirky language.
The above is not to disagree with functional programming in general. On the contrary, functional programming in general is highly valued. I just disagree with the dogma of the “purely functional” ones. Impure functional languages such as Scheme and ML haven’t these problems. They have “benign side-effects”. In fact, in Scheme functions are called “procedures”, not “functions”. This is because its designers know that they are not functions in the mathematical sense, and they intended to make them not necessarily pure. The purely functional language community often try to steal the word “functional programming” from traditional functional languages (Lisp, Scheme, ML), as if only purely functional languages deserve the name. This is not fair and this is harmful. We should be able to use the word “functional programming language” to refer to any language with correct implementation of first-class functions.
Everything starts to do harm when they are pursued to the extreme. Purely functional programming tries to fit the world into its model, but the world works in a completely independent way. It is wrong to think of everything as a nail when you have a hammer. Only by observing the reality can we get out of the religions that are limiting us. Don’t fit the world to your model. Fit your model to the world.
As mentioned in a post several years ago, I made an advanced Python static analyzer at Google. It turns out that this piece of code is still the most advanced static analysis for Python until today. But because of one highly tricky bug inside the analyzer, it had serious performance issues.
Only recently I revived my interest in it and fixed the bug by commenting out two lines of code ;-) After mutual agreement with Google, I can now release PySonar’s second version code (call it PySonar2). The code is now open for downloading on my GitHub repo:
The build process is not friendly at the moment, but please bear with me to fix it.
I have been working on it sporadically in the past few days, fixed several bugs. It can now produce good results for Python 2.5, 2.6, 2.7 standard libraries and projects like Django framework, with pretty good performance (should finish said projects in several minutes on a laptop).
Although PySonar2 contains some of the world’s most advanced static analysis techniques, Python is a very complex language to analyze, so corner case bugs are almost unavoidable. Please file an issue on GitHub if you find one. I’ll try to fix it when I get time.
