8 ms·

How long do you think it's going to take before program formal proof becomes the new standard in commercial applications quality standard? Today is focused on

by bsaul 13y ago

How long do you think it's going to take before program formal proof becomes the new standard in commercial applications quality standard? 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 ?

hosay123 13y ago
You should probably ask the people who've been promoting these ideas since at least the 70s :) "No time soon" is my best bet 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.
- DebianUser 13y ago
  The theory which was promoted in the 70s (whatever it was) was certainly vastly different from what's used nowadays. Thierry Coquand (who conceived the original theory behind Coq) was only 9yo. In 1970.
jbri 13y ago
I think it's going to be a long time coming, since the negative effects of mostly-working-but-not-quite software tend to be borne by the purchaser and not the creator, which means the extra expense of formal verification is not commercially viable when compared to just having a rigorous (or not-so-rigorous) testing regime. 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.
- bsaul 13y ago
  Ok, but it looks more like a chicken-and-egg problem. Think about this : Let's say i create a java/scala/whatever web framework that is even just "30% formally proved" (i know that's pretty vague, but bear with me) : don't you think it would be such a competitive advantage in the corporate world, that it would instantly be a commercial hit ? Then once one popular code lib or framework starts doing it, we all know the rest will follow and the trend will be set.
  - cbhl 13y ago
    Three points: 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).
    - tel 13y ago
      I want to qualify your (1) a bit—there's actually enormous value in "partially proved" systems in a sense. At the very least, that 30% is something you won't have to think about every again so long as the spec it's met works for what you need. 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.)
hershel 13y ago
Not an expert, but: 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++.
- munin 13y ago
  I have been told that this is only the case in America (and I guess Asia). in Europe, there are laws that require the use of safety-validation tools and worst-case execution time tools on code that will be used in safety critical applications, for example, flight control, process control, etc.
  - hershel 13y ago
    Safety verification tools - like static analysis/timing analysis - is different from full formal verification. Those tool run on their own and don't need complex definition of what to verify , and they verify just small amount of bugs.
- cantankerous 13y ago
  Look at aerospace and aeronautics. It's becoming par for the course there.
- sliverstorm 13y ago
  I don't know if formal code verification is much like hardware verification, but modern hardware like microprocessors and larger FPGA designs undergo verification... and it is so impossibly computationally expensive, the key exercise becomes selecting the most important 0.1% of coverage. 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.
gemma 13y ago
Formal proofs predate how we think about unit testing (check out IBM's 'Cleanroom' process). The concept comes from an age when most programming was a lot more like applied math, and it still has a lot of traction in industries with very high reliability/correctness requirements. Unit testing took over because it's easier and cheaper to do, the results are good enough for most environments.
munin 13y ago
> What about less strict and more used languages like C or Java? there already exists a system for verifying C, Astree (http://www.absint.com/astree/index.htm 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...
- barries 13y ago
  See also Frama-C (http://frama-c.com/ http://frama-c.com/), which can use multiple automated and interactive theorem provers. It's really a proof obligation management IDE that you can use with multiple provers / proof assistants.
- joaoff 13y ago
  Dynamically allocated memory is difficult to verify automatically. There are some tools based on separation logic (e.g. Smallfoot, HIP/SLEEK, jStar) that are able to verify C programs (or C-like programs). Current developments in this area are focusing on automatically inferring specifications (also known as abductive reasoning). Moreover, automatically verifying concurrent programs is also difficult and a hot research topic at the moment. If I am not mistaken, Smallfoot is the basis for a professional product being developed by Monoidics (http://www.monoidics.com 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/Friends_of_Invader.html http://www0.cs.ucl.ac.uk/staff/p.ohearn/Invader/Invader/Frie...
vidarh 13y ago
A long time, because it's been around "forever" and yet has gotten only a very little traction because it is hard, and for most things lack of verification is "good enough". 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.
Fixnum 13y ago
For imperative languages, the most popular approach to formal proof is to add partial correctness annotations in an axiomatic semantics such as Hoare logic. I've heard that Microsoft does this to verify many properties of the Windows kernel. (I think the most popular tools are 3rd-party and proprietary at the moment.) Of course, finding the right theorems to write down is not easy either. 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/ http://vst.cs.princeton.edu/
barries 13y ago
It's not feasible for large programs in any generally used language, especially imperative ones. This is because most languages have undefined constructs and constructs that are so flexible that proving useful things about them is hard. 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.
qznc 13y ago
There are various tools in the research world, but little real world use. Isabelle/HOL - Coq competitor like GCC and LLVM (http://www.cl.cam.ac.uk/research/hvg/Isabelle/ http://www.cl.cam.ac.uk/research/hvg/Isabelle/) ATS - C with proof assistant (http://www.ats-lang.org/ http://www.ats-lang.org/) KeY - Java with verification annotations (http://www.key-project.org/ http://www.key-project.org/)
- iso-8859-1 13y ago
  Interestingly, HOL Light is used to prove that the density of a packing of congruent spheres in three dimensions is never greater than pi/sqrt(18), a 400 year old problem: https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet 300,000 lines of code, still unfinished.
geoka9 13y ago
I think never. Between the "ship early" ethos and SaaS becoming increasingly popular, software quality has been going downhill for quite a while. Most parties seem to be OK with it, so I expect it to get even worse.
- cantankerous 13y ago
  These two concerns aren't separate. You can publish agile software frameworks like rails with assurance guarantees based on proofs. If programmers play within the bounds, they can retain various proof-grade guarantees about the software they write. Just make better tools for Chrissakes.
- Silhouette 13y ago
  Most parties seem to be OK with it, so I expect it to get even worse. 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.
- brandonbloom 13y ago
  I view "ship early" (and iterate!) as a superior verification strategy than formal methods for most typical software. Most errors occur much earlier in the pipeline than the authoring of the first line of code.
brandonbloom 13y ago
How do you formally prove that a GUI is "usable"? How do you formally prove that a game is "fun"? How do you even know what you should be formally proving? 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.
- cantankerous 13y ago
  I think the OP is asking about when what you mentioned in your second paragraph is going to become the industry standard. Nobody's going to be using formal verification to prove that something is usable or fun. 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.
  - brandonbloom 13y ago
    > Boeing) has been doing this for a long time 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.
  - Altenuvian 13y ago
    could you point to documents explaining proof checking in aerospace industry? I am especially interested in the history leading to software verification in avionics, the involvement of insurance companies and government regulation. thx
tel 13y ago
Coq is based on OCaml and similar to it but actually forms its own completely independent language. Others in the same vein are Agda, Idris, Epigram, Isabelle. Each one shares more similarities with the others than with their "host" language (if one exists) of which they're usually syntactic cousins. 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.
- bsaul 13y ago
  Thanks for the theorical background. I just had a look at the Curry-Howard Isomorphism article on Wikipedia, and i finally understood what my OCaml teacher muttered once in the classroom 10 years ago :)) 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 :)
cantankerous 13y ago
I think we're more likely going to see formally verified software development frameworks...something like a "verified Rails" before we see programmers using proof-checking in the general case. Basically it'll be the model-checking software built into a framework and a tool that will tell you if your code plays well / is safe according to the model or not. 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.
- tel 13y ago
  You're thinking something like Ur/Web?
  - cantankerous 13y ago
    Oh cool! I didn't know about this. Thanks for sharing. I'm going to read into it now :).
  - asdasf 13y ago
    Ur/Web has nothing to do with formal verification does it?
    - lmeyerov 13y ago
      Ur/Web uses dependent types (Ur) to build statically checked web libraries that prevent common bugs such as malformed or stale links. The exciting part (IMO) is that the 'row types' allow encoding your database schema in the type system, so it prevents bugs common to frameworks with heavy code generation, such as the ORM in Rails or template libraries in C++. 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.)
lelf 13y ago
I feel many people here miss the point: it's not edit edit edit ./src/Browser maybe annotate it with some smth ./verify some-property ./src/Browser.ml && echo 'seems OK, ship it!' It is coq proof.coq > ./src/Browser.ml The source code is just a side effect of proving some theorem. 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
- bsaul 13y ago
  thanks, didn't realize that.

by bsaul 13y ago

hosay123 13y ago

You should probably ask the people who've been promoting these ideas since at least the 70s :) "No time soon" is my best bet 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.

DebianUser 13y ago
The theory which was promoted in the 70s (whatever it was) was certainly vastly different from what's used nowadays. Thierry Coquand (who conceived the original theory behind Coq) was only 9yo. In 1970.

jbri 13y ago

I think it's going to be a long time coming, since the negative effects of mostly-working-but-not-quite software tend to be borne by the purchaser and not the creator, which means the extra expense of formal verification is not commercially viable when compared to just having a rigorous (or not-so-rigorous) testing regime. 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.

bsaul 13y ago
Ok, but it looks more like a chicken-and-egg problem. Think about this : Let's say i create a java/scala/whatever web framework that is even just "30% formally proved" (i know that's pretty vague, but bear with me) : don't you think it would be such a competitive advantage in the corporate world, that it would instantly be a commercial hit ? Then once one popular code lib or framework starts doing it, we all know the rest will follow and the trend will be set.
- cbhl 13y ago
  Three points: 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).
  - tel 13y ago
    I want to qualify your (1) a bit—there's actually enormous value in "partially proved" systems in a sense. At the very least, that 30% is something you won't have to think about every again so long as the spec it's met works for what you need. 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.)

hershel 13y ago

Not an expert, but: 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++.

munin 13y ago
I have been told that this is only the case in America (and I guess Asia). in Europe, there are laws that require the use of safety-validation tools and worst-case execution time tools on code that will be used in safety critical applications, for example, flight control, process control, etc.
- hershel 13y ago
  Safety verification tools - like static analysis/timing analysis - is different from full formal verification. Those tool run on their own and don't need complex definition of what to verify , and they verify just small amount of bugs.
cantankerous 13y ago
Look at aerospace and aeronautics. It's becoming par for the course there.
sliverstorm 13y ago
I don't know if formal code verification is much like hardware verification, but modern hardware like microprocessors and larger FPGA designs undergo verification... and it is so impossibly computationally expensive, the key exercise becomes selecting the most important 0.1% of coverage. 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.

gemma 13y ago

Formal proofs predate how we think about unit testing (check out IBM's 'Cleanroom' process). The concept comes from an age when most programming was a lot more like applied math, and it still has a lot of traction in industries with very high reliability/correctness requirements. Unit testing took over because it's easier and cheaper to do, the results are good enough for most environments.

munin 13y ago

> What about less strict and more used languages like C or Java? there already exists a system for verifying C, Astree (http://www.absint.com/astree/index.htm 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...

barries 13y ago
See also Frama-C (http://frama-c.com/ http://frama-c.com/), which can use multiple automated and interactive theorem provers. It's really a proof obligation management IDE that you can use with multiple provers / proof assistants.
joaoff 13y ago
Dynamically allocated memory is difficult to verify automatically. There are some tools based on separation logic (e.g. Smallfoot, HIP/SLEEK, jStar) that are able to verify C programs (or C-like programs). Current developments in this area are focusing on automatically inferring specifications (also known as abductive reasoning). Moreover, automatically verifying concurrent programs is also difficult and a hot research topic at the moment. If I am not mistaken, Smallfoot is the basis for a professional product being developed by Monoidics (http://www.monoidics.com 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/Friends_of_Invader.html http://www0.cs.ucl.ac.uk/staff/p.ohearn/Invader/Invader/Frie...

vidarh 13y ago

A long time, because it's been around "forever" and yet has gotten only a very little traction because it is hard, and for most things lack of verification is "good enough". 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.

Fixnum 13y ago

For imperative languages, the most popular approach to formal proof is to add partial correctness annotations in an axiomatic semantics such as Hoare logic. I've heard that Microsoft does this to verify many properties of the Windows kernel. (I think the most popular tools are 3rd-party and proprietary at the moment.) Of course, finding the right theorems to write down is not easy either. 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/ http://vst.cs.princeton.edu/

barries 13y ago

It's not feasible for large programs in any generally used language, especially imperative ones. This is because most languages have undefined constructs and constructs that are so flexible that proving useful things about them is hard. 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.

qznc 13y ago

There are various tools in the research world, but little real world use. Isabelle/HOL - Coq competitor like GCC and LLVM (http://www.cl.cam.ac.uk/research/hvg/Isabelle/ http://www.cl.cam.ac.uk/research/hvg/Isabelle/) ATS - C with proof assistant (http://www.ats-lang.org/ http://www.ats-lang.org/) KeY - Java with verification annotations (http://www.key-project.org/ http://www.key-project.org/)

iso-8859-1 13y ago
Interestingly, HOL Light is used to prove that the density of a packing of congruent spheres in three dimensions is never greater than pi/sqrt(18), a 400 year old problem: https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet 300,000 lines of code, still unfinished.

geoka9 13y ago

I think never. Between the "ship early" ethos and SaaS becoming increasingly popular, software quality has been going downhill for quite a while. Most parties seem to be OK with it, so I expect it to get even worse.

cantankerous 13y ago
These two concerns aren't separate. You can publish agile software frameworks like rails with assurance guarantees based on proofs. If programmers play within the bounds, they can retain various proof-grade guarantees about the software they write. Just make better tools for Chrissakes.
Silhouette 13y ago
Most parties seem to be OK with it, so I expect it to get even worse. 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.
brandonbloom 13y ago
I view "ship early" (and iterate!) as a superior verification strategy than formal methods for most typical software. Most errors occur much earlier in the pipeline than the authoring of the first line of code.

brandonbloom 13y ago

How do you formally prove that a GUI is "usable"? How do you formally prove that a game is "fun"? How do you even know what you should be formally proving? 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.

cantankerous 13y ago
I think the OP is asking about when what you mentioned in your second paragraph is going to become the industry standard. Nobody's going to be using formal verification to prove that something is usable or fun. 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.
- brandonbloom 13y ago
  > Boeing) has been doing this for a long time 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.
- Altenuvian 13y ago
  could you point to documents explaining proof checking in aerospace industry? I am especially interested in the history leading to software verification in avionics, the involvement of insurance companies and government regulation. thx

tel 13y ago

Coq is based on OCaml and similar to it but actually forms its own completely independent language. Others in the same vein are Agda, Idris, Epigram, Isabelle. Each one shares more similarities with the others than with their "host" language (if one exists) of which they're usually syntactic cousins. 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.

bsaul 13y ago
Thanks for the theorical background. I just had a look at the Curry-Howard Isomorphism article on Wikipedia, and i finally understood what my OCaml teacher muttered once in the classroom 10 years ago :)) 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 :)

cantankerous 13y ago

I think we're more likely going to see formally verified software development frameworks...something like a "verified Rails" before we see programmers using proof-checking in the general case. Basically it'll be the model-checking software built into a framework and a tool that will tell you if your code plays well / is safe according to the model or not. 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.

tel 13y ago
You're thinking something like Ur/Web?
- cantankerous 13y ago
  Oh cool! I didn't know about this. Thanks for sharing. I'm going to read into it now :).
- asdasf 13y ago
  Ur/Web has nothing to do with formal verification does it?
  - lmeyerov 13y ago
    Ur/Web uses dependent types (Ur) to build statically checked web libraries that prevent common bugs such as malformed or stale links. The exciting part (IMO) is that the 'row types' allow encoding your database schema in the type system, so it prevents bugs common to frameworks with heavy code generation, such as the ORM in Rails or template libraries in C++. 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.)

lelf 13y ago

I feel many people here miss the point: it's not edit edit edit ./src/Browser maybe annotate it with some smth ./verify some-property ./src/Browser.ml && echo 'seems OK, ship it!' It is coq proof.coq > ./src/Browser.ml The source code is just a side effect of proving some theorem. 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

bsaul 13y ago
thanks, didn't realize that.