Advogato's Number: The Future of Programming

It is an immensely difficult task to even state the correct behavior of a program in a formal way. Further, many formal methods for proving correct behavior involve concepts of pre-conditions and post-conditions and user input.

This is very complicated to define for a modern program - where multiple threads, input from the network, complex user input from multiple devices, and interaction with other programs can all play a role.

Now imagine that you actually have a statement of what it means for the program to be correct, as well as a formal definition of the possible user inputs. You could use these to prove the program correct. But they may be as complex as the program itself, if not more. So how can you trust _their_ correctness in turn?

Formal methods almost made sense in a world of batch computing where a program takes input at the beginning, runs, produces some output, and exits. In an event-driven, multi-threaded, multi-processing, SMP, networked, interactive world, they are nearly impossible to apply.

you beat me to it: I was gonna post on the exact same issue, today. funny. rather than repeat the intended posting in full, I'll just plant the links and let your fingers do the walking:

1. limited semantics + rich annotation (newer)
2. changing background assumptions about machinery (old diary-entry fodder)

though both these pages were written more as suggestions for future programming languages, rather than existing ones. Of existing languages, cayenne is the most practical such thing I've seen, as far as proving correctness at compile time. and its practicality is debatable.

if you want something which can do such proof-fu with C code, you want LCLint or larch. but it's not pretty. you really want a compiler to write your verification conditions for you.

proof repository? yes. PCC? yes. yes yes. this is stuff we sorely need.

To certify the reliability of your code you need to test it. If you can automate that testing then you can easily verify its correctness. Automation also takes some of the pain out of it. Many c programmers use asserts to help diagnose programming errors that result in conditions that shouldn't occur. Others advocate writing the tests before you write the code. If the language is object oriented then for each class you may like to write a method called test() that runs a suite of tests on the class to verify its correctness.

Here are some links to what people have said on the WikiWikiWeb about testing: FunctionalTests UnitTests

There are a quite a few Testing Frameworks available to help automate the tests.

"To certify the reliability of your code you need to test it." Not with formal proofs of correctness: testing doesn't constitute proof (unless you test every logically possible valid input), and proof doesn't require testing. Automated testing may be useful, but it's not at all the same thing as formal methods.

Thus Knuth says we should

Beware of bugs in the above code; I have only proved it correct, not tried it.

I wrote up a nice reply, but forget the title. Advogato wouldn't let me preview it and said to go back and try again. My browser didn't keep the original text, so I'll have to try again. :(.

I'm not going to be anywhere near as complete as my original response. Basically, I agree strongly with mjs. Using formal verification is very expensive and only works with well defined requirements. I've never been given requirements which were good enough. In all cases, there are an infinite number of programs which meet the requirements, but which aren't equivalent (because of how they deal with the under specified components).

And some of the requirements, like "a modular design which promotes reuse" isn't something you can formally describe.

Consider a relatively simple problem - getting a temporary file name. You need the directory and a unique name for that directory. Sounds easy, right? Which directory? /tmp, /usr/tmp, /var/tmp, $TMPDIR or /Program File/Temp?

Given the directory, how do you get the name? Call tmpnam? How random is the result? Some systems use "AAA", "AAB", "AAC", ... while others are only slightly better and use some combination of the PID and the current time in seconds. These allow both local and remote exploits. Local by using a race condition between getting the name and making the file. Here's a description of the problem for lynx. Remote because if the name is predictable and visible to the outside, then the black hats may easily guess names and see others' data.

Suppose instead the tmp file is supposed to be a well-known name, as when a client uses it to connect to the server. PVM uses /tmp/pvmd. $uid for this purpose. Now suppose the tmp directory is shared across several machines - this is frowned upon, but I've been at one site which did this for a couple of months. That assumption of uniqueness is no longer valid. I've seen a lot of program which used /tmp/foo.$$ for the tmp file. Not only is it predictable, not only does it present a possible denial-of-service (by preemptively creating the file), but it isn't guaranteed to be unique if two programs run by the same user on two different machines just happen to have the same PID.

Once you tell me how this can be formally described, then show me how to apply it to the exploits against emacs, vi, more and man. Like I said, it's a well- known exploit, but it still crops up again and again.

You said Thus, I believe that bug-free software is a prerequisite for security. This isn't correct. You can have code which is wrong (like int f(void){return 0;} when the required result is to return 1) but have no exploits, at least not when taken alone. On the other hand, a program running as root which sits on port 1234, accumulates the text passed to it from a given connection, and calls system() on the text when the connection closes, is a reasonably well defined program, but which is a huge security hole.

What a wonderful article! (It's great to see my old prof's book in the references too -- I just wish I'd been in a class where he taught formal proofs.)

I'm afraid I have to agree with the naysayers on several counts. Everything mjs says agrees with what little I learned about this stuff in college. I do hope that future developments will (or already have!) render some of his points moot. There's no reason the state-of-the-art can't improve after all.

I wonder if Advogato's idea of provably-correct snippets that can be used to build up programs would really fly. It seems to me that there could be ways to combine two correct peices of code and get a result that was not correct at all, but this is just a hunch.

Dalke:

"a modular design which promotes reuse" isn't something you can formally describe

On Dalke's temp file example: Ok, so you've identified one input variable (temporary directory), and two different functions (random tmp file name, and well-known temp file name). Handle the two differently. Ignore the nfs case, there is no foolproof way of creating safe temp files over nfs. No, you don't use tmpnam, it hasn't been proven correct, and it varies depending on libc anyway. Write your own random number generator, and prove it correct. Actually making the temporary file is going to depend on several system calls, and unless your OS has been proven correct, you have to assume they fully comply to their published interfaces, so this isn't a very good example anyway..

I'd say a better example would be a web server that serves data out of a in-memory data structure and runs from inetd. I've added those constriants so once it has started up, it need not rely on any system calls or other outside stuff that cannot be proven correct (well except stdin and stdout). I would love to see a provably correct version of such a thing.

Anyway, thanks for a great article. I'm going to try to think "how would I prove this correct?" when I start my next project.

Obviously, I don't fully agree with mjs here, though he does have some good points. If you want the requirements to fully specify the behavior of the program, then absolutely, it's hard as hell to get the requirements right.

But I think it's possible to prove a number of basic but interesting properties of programs, including never segfaulting, never overwriting the stack, never accessing freed memory, and not leaking. In the case of threaded programs, you can prove lack of deadlocks and race conditions (Greg Nelson did a bunch of work in this area).

I think there are interesting, simple things to prove for GUI programs, such as never keeping a grab. I also think it would be very interesting to prove that incremental screen repaint is visually identical to repainting from scratch - especially as this property fails to be true for many, many real apps.

Finally, I do believe it's possible to prove useful things about security, but to be meaningful, these properties have to be proved over an entire system, not just individual components. As I suggested, this probably means redesigning the system to be structured so that such a proof is tractable. I do not believe that it is practical to apply these kinds of techniques to existing systems.

To dalke: yes of course it's possible to have "bug-free" but insecure programs or the converse. All you have to do is leave security out of the requirements, as you suggest. However, that wasn't my point. What I meant to say is that any process which produces software with a substantial number of bugs is incapable of reliably producing secure software.

Regarding tmp exploits: yes, you have to consider the operating system as part of the system being proved. If you do that, then I think it's quite reasonable to prove the system correct against /tmp exploits.

Incidentally, it seems that the underlying problem with /tmp exploits is that Unix provides the wrong semantics for this type of operation. When you write to a tmpfile, then read it back, what you really want is the same file as you wrote. However, Unix doesn't provide access to file objects, it only lets you access a file with the same name, which might not be the same thing. The Exokernel does export file objects to user space, so you can avoid the problem altogether.

If you were programming a Unix system using formal proofs, you'd get stuck at this point in the proof. You could then do a search to see if anyone had tmpfile code that had been proven correct relative to Unix semantics, and just use that. Or, you could move to a post-Unix system in which these kinds of proofs were a lot easier. Either way, I think you would win.

To schoen: I am well aware of Knuth's famous quote. I think there are two issues here. First, you can get your requirements wrong. Testing is still an excellent way to uncover these kinds of bugs. Second, you can be unsure of your proof. To continue the FLT example, Wiles's first proof contained serious bugs, and even today some small doubt remains, due to the complexity of the proof. That's why I suggest a proof repository, where the proofs can get automatically checked.

Unfortunately, the best you can get from a "proof of correctness" is that a bit of code fails to contradict a specification.

The dream of proven-correct programs, dear to all our rigorous hearts, founders not on the shoals of the practical difficulty of the proofs -- although that has stalled progress -- but on the fundamental difficulty of producing correct specifications. (Certainly the majority of bugs in my code in recent years have been directly traceable to specification errors.)

This is not to say that formal methods cannot be helpful. Raph touches on a way they are in fact useful, now: abandoning the mathematical tradition that produces traditional proofs, we can co-opt just their rigor. We may never prove that whole programs correctly solve real-world problems, but we can prove that bits of programs correctly achieve precisely-described abstract goals that are useful in many (indeed, most) real-world programs.

Alex Stepanov, with his STL (which finally found its practical expression in C++ after decades of failed attempts in other languages (including, it must be noted, LISP)) had just such ideas in mind. How do we take advantage of bits of (proven) correct code, in programming? We put the correct code in libraries, and precisely describe their behavior and limitations. It is very hard to specify a library component both rigorously and usefully, but usually not very hard to implement it (provably) correctly. The STL demonstrates this, and is worthy of study just on that ground, completely aside from its demonstated usefulness in coding. The STL is just an example. Dave Musser at RPI has worked on formalizing this further.

It is its power in expressing libraries that makes C++ better-suited for this job than any other deployed language (although e.g. Dylan may challenge it someday). Interestingly, the object-oriented features of C++ are mostly incidental to this goal -- only the constructors and destructors, in particular, help much. Otherwise, it is its template mechanism that makes C++ so powerful. (Anybody who thinks C++ templates are just fancy macros demonstrates an entire failure to understand their power.) The other language features are not useless; they address other issues than basic correctness, such as organization.

We see hints of proof methods in lists of Class (or Component) Invariants that careful coders make a part of designs. An invariant breaks up the correctness problem at a class-interface boundary, reducing the problem to verifying that all component members maintain the invariants, and that code using the members (including other members) depends only on the invariants. Expressing invariants early, and maintaining their simplicity as the design evolves, keeps the design tractable.

Fruitful practical application of rigor will come not from promoting academic attempts at language design, but from tackling the real-world programming problem and demonstrating techniques that make us truly more productive with current languages. The STL and class invariants are two successful applications of the principle. I claim that a good C++ programmer produces easily an order of magnitude fewer bugs than an equally-good C programmer, by taking advantage of the language's automation and organizational tools, including the its uniquely powerful standard library and other libraries inspired by it.

Eventually, languages that better support rigorous techniques already being used industrially will arise and gain popularity; but the rigorous practices have to come first, and be applied in existing languages. (C++ itself arose in just this way: every good programmer claims to have been programming in object-oriented style all along.) [Footnote: Interestingly, Java lacks just those features that make C++ suitable for writing rigorously correct libraries such as the STL.]

We need only discover and apply those techniques, and eventually languages will arise to help automate them.

I'm not sure exactly what ncm means when he refers to "deployed" languages, but since he writes about Dylan (which no one could reasonably claim is widely deployed), I might as well speak up in favor of certain functional (or mostly-functional) languages, which have the very properties that ncm finds so appealing in c++.

The power of templates stems from the type-safety guarantees of parametric polymorphism -- which certainly predates STL (the Hindley-Milner type system paper was published in 1978) and, in my opinion, has found more elegant expression elsewhere. As ncm correctly points out, parametric polymorphism is orthogonal to object-orientation. On the other hand, he writes that "every good programmer claims to have been programming in object-oriented style all along," but I think that some proponents of functional programming would strongly disagree with that remark. One of the primary characteristics of objects is that they hold state. (I have read about "functional objects" in Objective Caml, but I don't see the point...) Functional programming, on the other hand, is all about eliminating state; in purely functional languages, there are no side effects at all. This property greatly increases the tractability of programs -- though, of course, it has its own set of problems. But, then, you can use mostly-functional languages (like SML) and use side-effects when you really need them.

I believe Raph and Maciej aren't really talking about the same thing. Raph is talking about the relatively straightforward task of proving specific formal properties of a given program. I interpret Maciej's comments as saying it is impossible to prove that a program does what it's ``supposed to do.''

At the heart of this issue is that there is no formal system for describing intent. The best we can do is write muddled phrases in the human language of our choice: Emacs is a self-documenting text editor; GCC is the GNU Compiler Collection; Advogato is a forum for free software developers.

Intent presupposes a whole bunch of implicit meanings, which can't be made explicit until somebody comes up with a formal definition of how consciousness works (proof of this statement is left as an exercise for the reader).

When we are dealing with intent, we are dealing with the heart of the human-computer interaction problem. However, we can still `prove' that a given piece of software satisfies the intent of the programmer, we just can't do it automatically (again, not until computers understand human language).

All a `proof' is, is the transformation of a theorem and a set of facts by the rules of logic until it is `obvious' that the theorem can be derived from the set of facts. Note that one person's obvious is another person's not-bloody-likely.

To me, it is obvious that Emacs is a self-documenting text editor, because I have seen Emacs' built-in documentation, and I have used it to edit text. QED. Another person may demand me to prove that Emacs is self-documenting, and I could say `run Emacs, and type C-h C-h'. If they were still skeptical, I could go even further, and show them how Emacs' source code defines its self-documenting nature. If they're still skeptical, I could try teaching them C, showing them how a C compiler works, showing them a specification of the machine architecture, teaching them electrical engineering, etc, etc.

Like most discourse, this results in either us agreeing that Emacs is self-documenting (that the proof is obvious to both of us), me realizing that I'm mistaken (because I failed to produce a valid proof), or us understanding that we don't define words in the same way (which is how two rational beings can disagree without contradiction).

So, the tools I want to see in the future (and part of what I'm working on now in Figure) are improved ways of literate programming that allow documentation of multiple layers of intent to be attached to source code, providing a proof that the code satisfies the intent. This hyperlinked documentation could be viewed at any granularity, from the source itself, up to the reference manual, up to a one-liner that describes the system. (There was some mention of this kind of system at the First Conference on Freely Redistributable Software, for those who remember it.)

I misrepresented Maciej... he seems to have only said that formal methods are difficult. I was addressing the perspective that they are impossible.

This whole talk of /tmp not being able to be proven is incorrect. Unix already provides symantics to make sure that your /tmp file is unique. There are various methods including making sure only root can modify the tree, /tmp being set sticky (to prevent others from removing files) and exclusive open. You can use predictable names as long as you make sure things are correct.

As for unix not being able to operate on file objects. This is not true, this is what unix domain sockets and pipes are used for. You can pass the file descriptor using them, and the temp file is safe. It can even be unlinked and still used.

As long as your processes are related, it is easy to pass a tempoary file between them.

As for the rest of the article, I agree immensily. We need to develope the ability to patch existing code that has been proven correct, add the necessary asserts to make sure that it remains correct for future programming.

This means if your binary tree can't take a NULL pointer, that all functions that use the binary tree need to be told that this function can't take a NULL pointer otherwise your program could end up incorrect. Creating extensions to support this will be really difficult if we continue to use C. We might be able to do it with a preparser, but what about shared libraries? We'd need to store that information in the library also in a way the compiler can get at it. The proofs need to be with the code, not with the definition of the interface (header files).

I think that functional programming languages are interesting. I haven't read them very closely, but it is definately an interesting topic.

Hopefully my rants wasn't to far off topic.

advogato said:

But I think it's possible to prove a number of basic but interesting properties of programs, including never segfaulting, never overwriting the stack, never accessing freed memory, and not leaking.

You can still have security holes in those systems.

As to the provability of C code having those problems, at best you can show the program may have a segfault, etc, but not that it will, just because of the halting problem. It does come up because people do write parsers which basically eval the input data, and if there just happens to be a 'while 1' in the program you get an effective DoS attack.

What I meant to say is that any process which produces software with a substantial number of bugs is incapable of reliably producing secure software.

You could then do a search to see if anyone had tmpfile code that had been proven correct relative to Unix semantics, and just use that.

But that sounds too pessimistic, and things will (hopefully) get better. So assume for the moment that such a system exists, and you want to use it to solve my tmpfile problem. You come up with a list specification in some unambiguous language and submit a search. Either you get no results or you get 1 or more results.

Suppose you get none. Why? It might be that no one solved the problem, but it might be that a similar but different implementation is available. For example, you may require the tmp file start with "XYZ" while someone else has code which takes a prefix as input.

(I know of 3 reasons for using a prefix. The first is partially for namespace control, although a true tmpname routine doesn't need it. It is useful when developing to disable tmpfile deletion, so you can easily find and view the file contents later for debugging. We had a problem once with pine where it froze up on NFS mounted disks, and it left tmp files hanging about. They started with ".pine" so it was easy to figure out the source of the problem.)

So your query has fewer inputs than the more general solution, and the output space is smaller - err, is a proper subset. Or perhaps you want the environment variable XYZ_TMPDIR to override TMPDIR to override the system appropriate /var/tmp, /usr/tmp, /tmp directory. This takes more inputs than an existing solution. Indeed, the solution may be to use two different verified parts - one to get the tmp dir and another to create the tmp file.

You need some way to find neighbor solutions. Because of the tight specifications of the query, you'll likely need some theorem proving capabilities in the search, and you'll want to allow similar proofs to match. Indeed, this comes up in real life a lot. If the GUI design spec says "button border widths must be 2 pixels wide" and the off-the-shelf toolkit only allows 1 pixel wide borders, then the spec could change because of the meta specification of "the implementation must take no longer than 3 weeks", precluding developing the originally required capability.

Now suppose you have 1 or more results to your query. You have to judge how appropriate a solution is. If it's an exact match then there's no problem with the I/O features, since that's what was in the specification, but it might be all commented in Russian, and you without Russian programmers. Or it may be some hideous web of gotos and unions of function pointers that you cringe after reviewing the first page of code.

If the exact matches don't meet these non-I/O requirements, then you need to start evaluting the non-exact queries to your search. How hard is it to change the code to meet your specs? Can you change your specs to meet the code? In the validation sense, how easy is it to prove the modified code agrees with the modified spec?

How much different is that than going to freshmeat and looking for "temporary file" or "tmpfile" or such, then scanning the results? You don't need to do through the effort of writing a tight spec for your problem. You search might even come up with some of the exploits people have used against tmp files, which probably helps you tighten your spec even better.

It might be quite hard to prove that your requirements are supported by the available components. Here's an example. I need to evaluate a math expression using C. I do a lot of Python work so I know how easy it is to use Python as a C library, pass in the string and evaluate it. Since I just happened(!) to design the math expression language to be identical to that used by Python, I let Python do the hard part. It's overkill - massively so - but I can do this in about 15 minutes of development time. Any full spec for Python will be huge, so for validation I would need to describe the range of input strings passed to Python (using some formal grammer definition) then let the validator chug for a while to check that, yep, there's no way to access anything else in Python other than expression evalutation with numbers.

Interestingly, for a full specification of a problem, you should often find that Python, Tcl, Guile or Lua, when used as a C library, can solve it! In the extreme case, a formal definition of each Lisp function should be sufficient for the search program to assemble a full solution by mixing and matching parts, assuming again you aren't addressing the stopping problem.

Not only would a proof be at least as complex as the original program, but in a very real sense any specification of the problem deep enough to serve as a proof *is* an implementation of the program. And having implemented it, not only can't you prove the proof correct, but you no longer need the original program except, perhaps, as an optimization.

For functions (I won't claim for entire applications), it's entirely possible to have a human-readable spec that's much shorter than the code, and a longer non-trivial and formally verifiable proof that the also longer code implements that spec correctly.

If the proof is as long as the program, that's not a problem, because the proof can be verified automatically. If the spec is as long as the program, that's definitely a problem, unless the spec is an intermediate machine-generated and machine-readable expression which was automatically generated from a simpler spec which a human can understand.

Yes, the correctness of long specifications themselves is a big problem, because usually people need to verify them by inspection. The correctness of long proofs isn't, because usually people don't.

Like many others, i would love to live in a world in which provable code would make bugs disappear. But i'm afraid i must agree with some of the other statements that have been made here: the specification of the problem is likely to be at least as complicated as the program itself. A great deal of software development consists of determining exactly what the desired behaviour is; that's probably the hardest part. That's design. Proceeding to implement it is relatively easy (and when you run into hurdles during implementation, more often than not, it's because you have encountered an additional decision about what the correct behaviour should be).

However, i do see a useful purpose for formal verification. They can improve the modularity of programs: successive versions of a module can be verified to behave in the same way (let's say you optimized to improve performance but you want to guarantee that it can be used as a drop-in replacement). Having a formal specification of the behaviour of a module also makes testing easier and more efficient: instead of testing the module in lots of combinations, you can directly simulate that behaviour as it reacts to the rest of the system and expect to get the same results when doing combined testing of the actual application.

In short, formal verification can be great for ensuring consistency, but can't guarantee correctness (at least in the "real world" sense of "doing the Right Thing" under a complex set of constraints).

One more thing i forgot to mention. Establishing consistency makes things more predictable, which helps us to build secure systems. We can't easily guarantee that a given program is secure; but once we know that a particular behaviour specification is or is not vulnerable to a particular exploit, we can then check that exploit against other behaviour specifications. And when upgrading or replacing security components, we can compare specifications to help ensure that we aren't introducing new holes.

This to clarify...

I didn't mention C++ because I think it's an ideal language. In fact, it was just barely strong enough to implement the STL. Similarly, it's just barely strong enough to do expression templates, and just barely strong enough to do template metaprogramming. It inherited some terrible problems from C along with some very fortunate qualities. I say fortunate because those qualities were not generally recognized as desirable at the time C++ was begun, and were left out of other languages designed at the time.

The reason for mentioning C++ was that it was the first language sufficient to implement the STL. I mentioned Dylan because it came after C++ and its designers seem to have learned at least some lessons from C++'s strengths and limitations. I mentioned Java because its designers clearly didn't. Much of what is (thus far uniquely) possible in C++ depends on rigorous documentation and coding conventions outside the language. Post-C++ languages will allow (at least some of) these conventions to be expressed directly in the language.

I hope to see the discussion develop in a direction that leads to practical results. This means acknowledging existing practice that anticipates Raph. It means identifying aspects of his goal that may never be practical, and separating them from what will become practical, and what could be practical right now. It means planning how to execute what could be done now but isn't yet.

We have a technology in place to propagate proven-correct code: libraries. What is missing? A habit of precise specification which allows the library components themselves, once demonstrated to be implemented correctly, to be used rigorously. As we develop ways to describe our libraries better, we can develop language features to allow them to be expressed directly. In the meantime, we have to do it the hard way. One thing we find with STL is that a library you try to describe rigorously comes out very different from what you would have designed otherwise. Specification changes design.

Somebody mentioned garbage collection.

The appeal of garbage collection is that it automates a particular variety of resource management. The programming styles it encourages fail where a program must manage other resources than memory. A programming practice which is able to manage other resources than memory can manage memory just as well, so garbage collection offers little. In a sense, only toy programs benefit much from garbage collection because most real programs manage resources other than memory. Good C++ libraries and programs built from them have no tendency to leakage, of memory or other resources.

Besides promoting rigorously correct libraries, what else can we do?

Making proofs about whole programs is still too hard. What we can do now is make proofs about tiny parts of programs. Each point where two paths of execution come together we have a need for a statement of some truth: what do we know about the state of execution at this point? After each loop, some condition has been established. Good programming, in this style, consists of establishing and building on demonstrable (and demonstrated) facts. Assertions can help automate checking these facts where they can be expressed in codable form.

At the end of a function, we should be able to say we have established a fact that happens to match the specification. Writing specifications so that they end up being matched by provable facts makes for functions that, though perhaps less featureful, can be used in other code being proven correct.

I already mentioned the very powerful technique of Class Invariants, extended to Component Invariants. It allows you to work on one member of a component without first memorizing the implementation of every other member, because the only facts the other members are supposed to rely on are listed explicitly in the invariants. This, in turn, allows us to build bigger components safely.

Only a few kinds of invariants are expressible directly in C++. As we get large bodies of code with lists of invariants, we can learn which are important to incorporate into language features to express them directly.

Unfortunately the problem with formal checking to obtain bug free programs is that the test condition(s) have to cover all the problem which have to be checked for.

The direct effect is that *writing the correct test* is no longer simpler than the program, it is actually of the exact same complexity, just usually written in a formal language instead of say C or Ada ...

Okay a note, I followed an advanced course during my PhD, precisely on formal verification. We applied the theory to a very simple example which was mutual exclusion on a state machine, very simple 4 states A B C and D either on or off, (directed) arcs from A to B and B to D and A to C and C to D. The obvious test was not to allow token A->B nor A->C transition simultaneously, all the room agreed. Then followed half an hour of formal computation done on the black board (painful !). At the end we got the proof that it was formally proved... Except that we discovered once finished that, well initial A=0 B=1 C=1 D=0 condition followed the formal proof and vas definitely not mutual exclusion. At that point it was very clear that debugging a program and debugging a formal test were of the same complexity ... Unless your program is described by the formal tests applying on it, well you have a serious problem.

However by doing some formal proof on your code you still enhance it, it's like a very thorought review, it does make sense in some cases (protocols implementations and embedded finite state machines especially). But it won't bring you zero fault software for the very simple reason that achieving that need to specify a zero fault test for this program which is of the same complexity than implementing a zero fault program.

I like the idea of proofs, and I don't agree with all criticisms of them. In particular, I don't think it's necessarily so that the specification is as complicated as the program. E.g. the specification may be "output is sorted in ascending order and has a one-to-one correspondence with the input [and is produced in some suitable time bound]". Such a thing is not the same as an algorithm, and can be substantially simpler than the corresponding algorithm. So it is meaningful to try to make systems where we write a simple specification, check that very very carefully by hand to see that it's really what we want, and then everything we do after that can be checked by computer to see whether it's correct. I'm just not convinced that it's practical yet.

I'm not convinced that proofs are practical. I'd appreciate a pointer to a proof system powerful enough to express a proof of the correctness, with mean average and worst case performance bounds, of a good hash table algorithm. (And for that matter, sometimes when I worry about security, I worry not only about standalone computers, but about networked computers, connected to networks with less than airtight physical security. In order to start proving the security of my network protocols, I'd appreciate a pointer to a proof that P/=NP, and preferably also that it's impossible to compute discrete logs efficiently.:-)

Finally, I'd like to disagree about garbage collection -- it's not just for toy programs. For many programs -- e.g. compilers, programs to optimize circuit board routing, and various scientific and engineering simulations -- there are no significant resource management issues other than memory management, so it's largely irrelevant whether other resources are managed on the same footing as memory. And although constructors and destructors are OK for handling memory which is owned by a single object, and can be kludged into handling memory shared by several objects (by using reference counting and the like), if don't have GC when you are working on a problem where the data naturally have cyclic relationships, you end up dealing with resource leaks bending the algorithm out of shape to avoid them, and or writing your own little GC. Ick.

If you follow discussions on bugtraq, you'll see that the majority of security problems are buffer overflows. If you want secure programs, use a language that provides bounds checking. If you want programs that don't segfault, use a language without pointer arithmetics and with garbage collection.

The most often heard argument against those features is performance. Let me quote some (admittedly best-case) benchmarks:

  Five Million Integer Sieve of Eratosthenes
  ==========================================

   Implementation           Seconds
  --------------           -------
  C                           3.90
  Dylan w/o bounds checks     4.33
  Dylan w/ bounds checks      4.35
  Python w/ 'while' loops   156.83

A lot has been happening in compiler research. There are hard realtime garbage collectors (it's already a problem to implement hard RT manual memory management!), and there are incremental garbage collection algorithms that don't pause your application.

If you think you have no problems doing proper bounds checking in C manually, try to spot the bug in the following code snippet (scut/teso on bugtraq):

This code is insecure:

 void
func (char *domain)
{
        int     len = domain[0];
        char    buff[64];


         if (len >= 64)
                return;

         strncpy (buff, &domain[1], len);
        buff[63] = '\x00';
}

A form of code proving is already in widespread use - static type checking does a good job of preventing type casting bugs. In that spirit, defined enumerations and parameterized types are also good ideas, as are static declarations of whether an object's constructor has completed. (The 'final' keyword in Java has some serious problems because the language lacks this feature.)

Writing a specification which is simpler than the code it's specifying is a real art. The project I'm working on right now has a messaging system with multiple layers of abstraction in it. Most of the tests are along the lines of 'put x in one end, assert that x comes out the other'. Usually even significant changes in the underlying code can be debugged with the exact same tests.

I have come to view static type safety as mostly a crutch for not having appropriate tests, but I still miss type safety for exceptions thrown, a feature Python does not have.

If one were to go whole hog and try to really prove a program, stating that it should never have an unhandled exception is an easy requirement to state and a very helpful property to prove a program has. It would have to be taken in the right spirit though - I have many times seen programmers catch exceptions and not provide any error handling code just to make the compiler stop bugging them.

It is important to note that security depends on keys which are passed around by human beings.

In all password systems (like advogato) you have a small subset of the total namespace that people actually use. Compromises come from key re-use on other systems, limited human capacity to remember long passwords, and insecure storage systems for email.

No remotely accessable service is *ever* provably secure because a random user *alway* has the chance of guessing the right code. So now we draw a threshhold based on how many tries they can execute in a day vs. how important security is in our application. Another option is to limit the geographic range of IP source addresses, however IP packets can be spoofed. There is a small (near-zero) chance of guessing correctly long enough to maintain a connection and slip in the required packets to fake an "allowed" login.

At this point you have to throw up your hands and say the current internet infrastructure is not provably *anything*. The Internet kinda sorta works, cross your fingers, no guarantees. The amazing thing is that by giving up the "guarantee" of circuit switched traffic we suddenly gained an amazing proliferation of successful new services.

Guarantees, proven theorems, these are not organic. Absolute Guarantees lead to things like mailand China being stagnant for 1000 years. Programs will stay organic they will get harrier, not because we don't try to constrain them, but because the intertwining complexities of problem domains will demand it! Basically infromation is not securable in a provable manner. The last limitation to that is the human mind!

Care to submit your administrators for a formal logic neural analysis? Insert a 10K needle probe into their soft pink flesh, run 3 years of tests, and after which conclude only 1% probability of a security leak from this human brain over the next 6 weeks. Phew! -pehr

ps.

There is no security on this earth, only opportunity. -Douglas MacArthur

Just the other day at one of the Kernel-Panic LPSG meetings (which I am attending so I can learn more about programming), the subject of programming languages was raised, and someone described succintly the class of "declarative programming languages". It was mentioned there that declarative programming languages and definitional programming, are succeptible of strict logical proof of correctness. As it was the first time I've heard about this, I went to Google and found some more info, from where the following is extracted:

The basic property of a declarative programming language is that a program is a theory in some suitable logic. This property immediately gives a precise meaning to programs written in the language. From a programmers point of the the basic property is that programming is lifted to a higher level of abstraction. At this higher level of abstraction the programmer can concentrate on stating what is to be computed, not necessarily how it is to be computed. In Kowalski's terms where algorithm = logic + control, the programmer gives the logic but not necessarily the control.
(From: A Note on Declarative Programming Paradigms and the Future of Definitional Programming)

I am not an expert programmer, nor I learned programming by attending classes, so my theoretical knowledge of programming language research is almost null, but I think that an idea like the one embodied by declarative programming would be great to help reducing most of the problems that we have with the existing languages.

Is this the solution for programming in the future? Will the future be divided among programmers generating the scaffolding/frameworks on which others will use declarative programming to generate applications? Am I way off base in my understanding of the whole situation?

My experience is that declarative programming languages is just a dream. The main reason is that also a declarative program may look cleaner, and sometime much more cleaner than an itterative one, it's not usable, except for very very small applications or very very modular applications, because it's much harder to debug, and debugging is the highest cost in a development, what people seem to forget when they are developping only prototypes, not production softwares.

Declarative programs is very much like mathematic theorems. Specifying the theorem is generaly short and fairly easy to read, but the problem is to check if it's right.

The assertion that declarative programming have a clear bonus which is that implementation can be changed with the application remaining the same, so provide better and better execution speed is half true.
It's true because it's possible: the clearest example beeing SQL.
But it's also false because itterative programs can also be speed up without changing the application source code. It's hard or not possible at all if the application uses low level programming, but if the application is short and high level programming, it's possible as well. So, the possibility to change the underlying implementation without changing the application is rather a matter of wether the application is high level or not.

So, my conclusion is that declarative programming can fit only for a very tiny scripting language, and that's exactly what SQL is, but even in such a case, a high level iterative language would work as well, also the optimizing functions would have to be written differently. The key difference in this case is historical: there have been many studies about dealing (rewritting) with logical programs, but rather few with itterative ones that used to be, historically, mainly low level.