Today is focused on unit-testing and test code coverage, but formal proof seems really even better.
I only have heard about Coq , which i think implies code has to be written in OCaml , but i suppose the same kind of tool exists / could be done for Haskell or Scala. What about less strict and more used languages like C or Java ?
Formal proofs (and type systems too) can only prove that your programs and formal specifications are internally consistent. The overwhelming largest set of failures in commercial software development are in requirements solicitation!
"Mathematics may be defined as the subject in which we never know what we are talking about, nor whether what we are saying is true." - Bertrand Russell
There is a very high initial and maintenance cost to proofs and it would be a mistake to insist that people pay that cost when better cost/benefit trade offs exist for most needs.
Automated proof checking and derivations systems have been under development and research for a long time now. It's almost just an engineering problem to introduce them in a way that commercial companies can use them.
The aerospace industry (ex Boeing) has been doing this for a long time, and they make it work quite well for them.
Sure, and Microsoft has been using formal methods for eliminating all manner of security holes since at least the XP SP2 days. I didn't say that formal methods were always a bad trade off. I said that they are very expensive and implied that they are a bad default tradeoff for general purpose tools to make.
I am especially interested in the history leading to software verification in avionics, the involvement of insurance companies and government regulation.
thx
If we were able to get rid of the 'THIS SOFTWARE IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED' thing that graces virtually every software license agreement, so that software publishers were actually liable to some extent for the software they produced, that would help to improve things. I don't see that happening any time soon though.
Then once one popular code lib or framework starts doing it, we all know the rest will follow and the trend will be set.
1. This is one of those things where you want it to be all-or-nothing. "30% formally proved" is completely useless; it just means that the inevitable bug or security hole is in the other 70%.
2. You're limited to writing constructs that can be formally verified. (My understanding is that this means that it's a bit more difficult than "let's formally verify Ruby and then run all the Ruby programs on our verified Ruby"; some programs will need to be rewritten and others will simply not be verifiable.)
3. We still have to solve the politics problems that already are pervasive in some of these environments (e.g. people who intentionally leave easy bugs in their code and then fix them later so that they look like they made more changes as measured by a KLOC count).
But what I really wanted to talk about is the exciting stuff going on in languages like Idris where programming is paramount and proving is just there for support. In a situation like this, your goal is less to arrive at 100% formally proven systems, but instead steal 90% of the power of a proof assistant to build more maintainable, powerful code. In this case, you're quite likely to only prove 30% of your code, the skeleton perhaps, and leave the rest. The result is often however that when you do this, the remaining 70% of the code is so restricted by your design that there are only a handful of ways to continue and they're likely all the right behavior.
A great example of this is Ur/Web which uses just a little bit of dependent typing to ensure that the names in your forms, domain, and databases all match up. It means you design your entire system around those names (your domain) and prove it to be formally consistent. Then the remaining design space is tiny and it's easy to write a good program.
... Or even to augment that skeleton with a security policy and have static flow control analysis "for free".
(That said, Ur/Web is a prototype system with minimal documentation, so I won't recommend it as an actual "system of the future"... just a glimpse.)
That said, each of them is far more similar to OCaml/Haskell than say, C.
They are all based to some degree or another on Martin Löf's Intuitionistic Type Theory which is a wonderful unification of mathematical logic and straightforward functional programming in the same vein as the Curry-Howard Isomorphism.
Generally, much of the forward research is aimed at making the proofs more automatic and easier to use. The problem is wildly intractable by brute force, so much cleverer tricks must be employed. Some of these are quite wonderful and suggest new ways of programming as a dialogue between a human and an intelligent compiler that I really hope become more common in the future, though the industry will be unlikely to drive it. See the literature on Epigram for some talk about this.
There's also an important distinction between proof systems and "dependently typed languages" where proof systems restrict their power greatly so as to ensure the things which are proved in them are mathematically consistent while dependently typed languages which are more "practical" seek only to provide proof-like heuristic support to programming. In the former, you'll likely see a complex way of describing group theory in the language of program types and the program itself is irrelevant because its mere existence is sufficient for logical purposes. In the latter, you'll see a strong synthesis of a program and its internal logic as expressed by its types which ensure that invalid programs are wildly difficult to write as you'll likely have to abuse some crazy flaw in intuitionistic logic in order to do so.
The most canonical example is the fixed-length vector where you can write things like "append takes two vectors and results in one that's the sum of their lengths" and thus track (statically!) that you have no out of bounds errors possible in your program. It's also incredibly useful for getting nice properties like "this vector-of-vectors representation of a matrix is not ragged" confirmed at compile time... something that even an advanced non-dependently typed language like Haskell or OCaml is (mostly) strictly in the domain of runtime checking.
But, to solidify, mafribe is much more correct than my comment and there's, as far as I'm aware, a much larger menagerie of other type theories. The recent Homotopy Type Theory publication—which was on HN as notable due to its publication process—was yet another step in this direction.
The part i didn't get in the equivalence between program and proof, is that a function can be seen as a proof that provided the input parameters are of a given type, the output type is going to be that one. Quite simple in fact, but it only clicked right now :)
edit edit edit ./src/Browser
maybe annotate it with some smth
./verify some-property ./src/Browser.ml && echo 'seems OK, ship it!'
coq proof.coq > ./src/Browser.ml
How long do you think it's going to take before program formal proof becomes the new standard in commercial applications quality standard?
Long enough
As I understand it, creating a proof becomes increasingly more complex in proportion to program size. You'll notice in this project, their proof only covers a few hundred lines of code. That's not because their program just happened to be a few hundred lines of code, but because they designed it to allow a practical proof.
Isabelle/HOL - Coq competitor like GCC and LLVM (http://www.cl.cam.ac.uk/research/hvg/Isabelle/)
ATS - C with proof assistant (http://www.ats-lang.org/)
KeY - Java with verification annotations (http://www.key-project.org/)
https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet
300,000 lines of code, still unfinished.
there already exists a system for verifying C, Astree (http://www.absint.com/astree/index.htm). Airbus, volkswagen, and similar companies use astree (they are, as I understand it, required to by EU law) to verify safety-critical software in their airplanes and cars. though astree has some large limitations on the C code it can verify, for example, no dynamically allocated memory or recursion.
investigating why it has these limitations is a good way to begin investigating what our current limitations are when formally reasoning about computer programs, and why C is so terrible to assure...
If I am not mistaken, Smallfoot is the basis for a professional product being developed by Monoidics (http://www.monoidics.com). Interestingly, the company was recently acquired by Facebook :)
Update: Here's a link with a list of related tools: http://www0.cs.ucl.ac.uk/staff/p.ohearn/Invader/Invader/Frie...
There's currently an attempt to formalize a subset of C, with an axiomatic semantics, all the way from specification down to machine language: http://vst.cs.princeton.edu/
Even if languages designed to abet formal proofs, like SPARK, were commonly used, proving anything but the most trivial properties requires a completely different mindset, significant additional training and experience. This puts formal proofs outside the abilities of the average engineer (including myself).
Finally, useful properties, like termination (lack of infinite loops/recursion), let alone termination within a time bound, or correctness with respect to non-trivial requirements is extremely difficult even for those with extensive experience in the area.
In addition to the difficulty of creating proofs, it is amazingly difficult to state non-trivial requirements formally and verify that the stated requirements are the right ones: often the source of the requirements (customers/users, supervisors, marketing) have neither motivation nor interest to state them formally or review formally stated requirements.
Are they OK with it, or do they just not see that they have a viable alternative at present?
I can think of numerous cases where from a personal and/or professional point of view I would have happily spent real money on upgraded/alternative software to what I've got if it fixed bugs that waste my time or make the results I get worse than they should be. Obviously some people will just rip off software whatever you do, but for paying customers, I'd be very surprised if quality alone couldn't drive a significant movement in a market, other things being equal.
I think it's all the unrelated things that aren't equal that are holding back that kind of competition. An interesting question is therefore at what point the willingness to use good software to develop more good software could cost less than putting up with poor quality incumbents, given that the real cost of both strategies is high. Even as a glass-half-full kind of guy, believing that a relatively small part of the industry could begin to pull that off without requiring the entire mainstream to shift, it would still have to involve far, far more people than are involved at the moment if we're going to create a sufficiently comprehensive foundation of development tools and essential libraries to bootstrap a whole quality-first ecosystem. The good news is that if you can establish that foundation, everything you do afterwards is easier in quality-first world has that advantage over the quick and dirty status quo, so momentum is on your side.
Just make better tools for Chrissakes.
Do you have a citation for this? Having spent plenty of time working around bugs in the older era of software development which took years to fix, I think your statement reflects nostalgia or inexperience. Those long, deliberative development cycles weren't some bygone golden age – and any codebase from that era has the thicket of "#ifdef BROKEN_SUNOS_FEATURE" blocks to prove it.
Having programmers use proof checkers to write proofs about their own software and then prove them is still very far away, if it'll ever happen at all. One can always dream happy dreams about the Curry-Howard Isomorphism, though.
The connection to formal verification is that dependent types (depending on how you do them) let you stuff custom computations into the type checking phase. The two coolest uses of dependent types (IMO) are to verify your code and, surprisingly, synthesize boilerplate.
(Btw, the guy making Ur/Web is quite important in the Coq community and Ur is one of his research vehicles for these ideas.)
Currently formal verification is complicated, expensive, and can only be used for verifying small amounts of code. And if you look at the places where it's highly valuable , i.e. security,hardware design and critical/medical systems - i don't see a wide deployment there. So not good signs.
And i heard of formal verification tools for c#, ada, and c/c++.
So, if they are similar pursuits, I can't help but imagine complete formal verification of large modern codebases would also be essentially computationally impossible.
What you may see more of is the approach taken in this project: Formally prove a tiny kernel that mediates system access, and sandbox everything else.
Though arguably, we're on our way to make that much easier through increasing support for varying levels of virtualization and finer grained authorisation (capabilities etc.), which means this approach will be able yield benefits even for software without a formal proof for the part that mediates system access.