The Old Joel on Software Forum: Part 3 (of 5) - Exceptions, Threads and robust software.

Exceptions, Threads and robust software.

Much like Joel, I don't like exceptions. I don't know Joel's stance on threads, but I don't like them either. And following Joel's articles, I'd speculate he doesn't like them as well for the same reasons.

There is a school of thought in programming, which I belong to, and few others do, that hold to the ridiculous idea that you should be able to prove your program correct. That does not mean you actually have to prove your program correct every time - it does mean that you should be able to, when the need arrives.
And "proof" here is in the mathematical sense, that which does not depend on opinion or hype - a correct proof is irrefutable. (This is very far from the legal sense of "proof", which - unfortunately, way too many programmers recently adopt).

This is a design criterion much stricter than you usually meet. And it almost rules out threads and exceptions. Because you can't just use "someone handles it" as proof - proof has to show that your system is in a consistent, predictable state after the exception has been handled. RIIA is good for these kinds of proofs, but only for "acquisition-style" operations, which are not a natural representation for most multi-stage processes.

Among other things, following this criterion leads you to better design choices, such as abolishing "look before you leap" practices, such as trying to detect if a file exists before trying to open it, except as optmiizations.

Exceptions make such proofs extremely hard, because - unlike error codes, you have to be aware of any exception that might be thrown by any code you use, even if it's 50 levels deep, -- any call will potentially not return to its caller. Java forces you to handle all of them, but it seems almost no one actually uses this, (this has been elaborated on in other threads, e.g. see Bruce Eckel's blog).

Threads make such proofs extremely hard, because any system state may change at any time, and to be certain that a variable doesn't change between two lines, you have to show that nowhere else in the code can change that variable. Note - not that nowhere else in the code *should* change it -- rather, that nowhere else in the code *can* change it. That requires scanning your entire project source code just to prove that "t = a; a = b; b = t;" exchanges 'a' and 'b', in some cases (e.g., when a and b are objects that are in a container accessible by other threads). You would have to have extremely fine grained, or extremely coarse grained, locking to make this proof feasible - either way, you're losing most of the advantages that threads offer.

Threads can be used in ways that are (relatively) easy to prove correct, and so can exceptions - but "provably correct" usage of either is unlike the way 99% of the population uses them.

"Provability" also drives design towards stateless functions as much as possible, because hidden state is very hard to reason with.

From my experience, programs designed with provability in mind, come out shorter, much more robust, much less buggy, and much simpler than when provability is not a design criterion. Testing can only prove a program buggy, but never correct. And, especially with threads and exceptions, testing shows very little. A correct proof shows a hell of a lot.

And I repeat, again - the criterion does not mean that you _should_ prove your program correct. It means that you should _be able_ to do that, if/when the need arises. Threads and, to a lesser extent, exceptions, make proofs infeasible, and that's why I don't like them, and I suspect Joel doesn't either.

There is the slightly stricter school of thought, which is practiced by DJB, which says you actually should prove a mission-critical piece of software correct. That's Dan's main reason for refusing to let people distribute modified versions of his mission critical software - no one else proves their modifications correct, and he therefore would rather have the end user apply the patches and recognize that they are not an integral part of the software.

Ori Berger
Tuesday, October 14, 2003

Before I respond, let me ask for some clarification. When you say that threads and exceptions inhibit the ability to prove that a program is correct do you mean in all cases, or just when they are misused (or some other subset of cases). Also, by "correct" I assume you mean that the implementation and the specification are in agreement. Finally, are we talking about in practice (i.e. using popular operating systems and tools) or in theory?

DBC
Tuesday, October 14, 2003

I mean that threads and exceptions, as they are usually used, make it _practically_ impossible to formally reason about programs in the real world.

Both are "misused" more often than not (in the "provability" sense), to the extent that "good" use can hardly be found at all.

"Correct" may mean that the spec and the program are in agreement, but that's not always the case. For example, if one of your users comes and says "I pressed the "Save" button, and got no error, but I can't find the file". Your spec probably doesn't address this specifically. But you _should_ be able to approach your source and prove, "with reasonable certainty", that this situation can't happen. Or, alternatively, prove that it _can_ happen, and be able to reproduce the behaviour based on the proof.

Regarding practice vs. theory - None of our modern tool is proved correct - there are a few microcontrollers, few telephone exchange programs, few medical programs, and that's about it, I think. So any real "proof" is always incomplete in the mathematical sense.

But in practice, you usually know what packages you can rely on to work as advertised, and whcih you can't, and need to plan your proof sketch accordingly. For example, I tend to assume that API calls work as advertized, but not better than advertized. e.g., ReadFile is not guaranteed to succeed even if the file is open and long enough because e.g. the file is on a remote share which might have been disconnected since the OpenFile, or on a floppy that has since been pulled out. But if ReadFile succeeds, I do trust that every distinct byte it returned was, at one point or another in time, in the proper location in the file (and I only assume that they all did in the _same_ point in time if I locked the file against changes).

I hope that clears things up. Thanks for the questions - it definitely needed to be cleared up.

P.S: In Win32, a function call that deletes a file can succeed without deleting a file. So you should always suspect the API specs as well -- though most API specs can, indeed, be trusted.

Ori Berger
Tuesday, October 14, 2003

I accept your arguments that having multiple threads touching the same data can make proving things hard.

But what practices do you suggest to use threads and exceptions in a way that does not prohibit this?

Mike Swieton
Tuesday, October 14, 2003

I don't see the difference, Ori. With "return code errors", they eventually propogate up to the same "conceptual" level that exceptions do to usefully deal with them. Return codes just seem to result in code bloat.

I think your thread criticisms only apply to situations where you shouldn't be using threads anyway, but that's a different argument.

Testing *can* prove a program correct, but its highly dependent on the meaning of "prove"; you're just verifying state transitions for various inputs on a state machine, after all.

Jason McCullough
Tuesday, October 14, 2003

I think the halting problem implies that you can not 'prove' a program correct.

Regarding exceptions, I like them because when writing a program <i>all</i> I want to think about is when things go right. Errors are a small proportion of executions.

When things go wrong is another stream of thought, thats what exceptions get me.

Thats not to say processing shoudn't be conditional on returned valudes.

Also, the language LUA has really nice multiple value returns.

Anu
Tuesday, October 14, 2003

Thanks for the clarification, Ori. In that context, there's little in your message that I can disagree with. The state of the practice with respect to using threads, exceptions, and quite a few other items, is abyssmal. What's worse, a lot of folks can't/don't recognize this.

One of the reasons that so many programmers "roll their own" for even simple things is that we've all come to mistrust the poorly engineered libraries that are available, especially when there's no source code for them.

That said, it's been my experience that when properly used, these things do not hamper the ability to make inferences about the correctness of my programs. This is especially true when used in conjunction with tools like design by contract, or "persuasive programming."

DBC
Wednesday, October 15, 2003

Ori, excellent post.

Threads, like exceptions, are scary because code inspection doesn't reveal the bugs. Threads are even worse because errors in thread coding can result in code that fails in an unreproducible way, which makes debugging orders of magnitude harder. The only kind of bug that can stay in code for months or years without a fix found or findable is timing-dependent thread bugs. You can debate threads on the merits but I find that they carry a remarkable penalty for screwing up and frankly I'm usually too scared to mess with them.

Two things I try to avoid for the same reason as exceptions: operator overloading, and extensive class hierarchies. Both of these make code do things which can't be seen by staring at the source code. I would rather use a simpler programming language or a subset of my programming language's facilities if it means that I can tell what code does by reading it, without having to have outside knowledge that, e.g., the assignment operator is overloaded to do mysterious things in mysterious ways. Anyone who has tried to code with Microsoft's built-in compiler classes that support COM and "hide" the need to think about reference counting through operator overloading knows what I'm talking about. You can stare at the code all day and never find a reference count bug.

Joel Spolsky
Wednesday, October 15, 2003

Anu:

Correct me if I am wrong, but I was under the impression that the halting problem was that you couldn't prove whether or not an arbitrary program would halt, and not whether a given program could be proved to halt or not. Can anyone clarify this?

Mike Swieton
Wednesday, October 15, 2003

"I would rather use a simpler programming language or a subset of my programming language's facilities if it means that I can tell what code does by reading it"

This is exactly where various kinds of assertion techniques shine because they make explicit the intent of the code and raise a flag when the intent doesn't match what actually happens. Design by Contract is one technique which is mostly about exposing the semantics of abstraction. The use of loop variants and invariants are another, similar technique for exposing the semantics of repetition. There are similar approaches for capturing and making explicit the intent of other programming constructions like selection, or inheritance. Even threading can be clarified if you are willing to study and follow what Hoare has to say about the semantics of his "Monitor" abstraction (which is what the threading model in Java is based on).

When you employ techniques like this a lot of the problems seen in connection with things like threading or exceptions disappear because they guide you towards using each of these tools as the tool is meant to be used.

Now, like Ori, I like to be able to reason about my programs. But even more importantly, like Joel, I like to be able to read my programs easily. Good assertion techniques enable both of these objectives to be achieved.

DBC
Wednesday, October 15, 2003

Some info regarding the Halting Problem.

http://c2.com/cgi/wiki?TheHaltingProblem

Anu
Wednesday, October 15, 2003

I've been programming professionally for twenty five years and I'm usually the first one to dismiss any programming practice I didn't learn from Kernighan & Ritchie. However I've come to appreciate exceptions over time. I think Joel and Ori are dressing up their personal preferences with technical arguments that don't hold up to scruitny.

Joel wrote: "...exceptions ... are scary because code inspection doesn't reveal the bugs." Actually staring at code that looks at return values doesn't reveal the bugs, or give you any assurance that all possible errors are handled. Compare:

ec = dosomething(a,b,c);
if (ec == 1)
// do something about error 1
else if (ec == 2)
// do something about error 2
...

By looking at this I can see that the programmer anticipates a few return values and handles them. I don't know if the programmer handled ALL of the possible return codes, or if there are other problems in dosomething() that aren't communicated in the return code, or even if what the programmer thinks error code 2 means is really what the called function is trying to signal.

Compare this to exception-based code:

try:
dosomething();
except oneExceptionType:
// do something about exception 1
except twoExceptionType:
// do something about exception 2
...
except:
pass; // maybe caller can deal with this

Both examples convey the same information to the reader with regards to what the programmer expects dosomething() may do. But the exception-based code does more. It attaches names to the exceptions. If the programmer was paying attention the exceptions are part of a standard hierarchy defined by the language, rather than random numbers chosen by the programmer. The exception-based code won't simply proceed if dosomething() throws an exception it doesn't expect--it propagates the error, which is something tedious and messy with error codes.

You can always use exception handling to simulate checking return values. A try... catch around a function call, catching all exceptions, is logically equivalent to a function call followed by a bunch of if/then/else statements. The big advantage of exceptions even in this case is that exceptions convey meaning and state information, and they are standardized in the language.

When using function libraries written by someone else, or OS APIs, there's tremendous value to EVERYONE following a single standard for reporting errors. No amount of staring at a bunch of if/elses following a function call tells me anything about what the underlying function may do wrong, but looking at the exception handlers does.

Another argument against error codes and for exceptions is coupling: two modules that both have to know the meaning of an error code--and have to be kept in sync if the meaning ever changes--are control coupled. No amount of looking at the code will reveal the potential problems caused by the coupling. Of course error code values can be standardized (or even made part of the language definition), but often they aren't. Exceptions are (though I grant some programmers feel compelled to invent their own exception hierarchies).

Ori objects to exceptions because they break provability: "Exceptions make such proofs extremely hard, because - unlike error codes, you have to be aware of any exception that might be thrown by any code you use, even if it's 50 levels deep, -- any call will potentially not return to its caller." Provability is purely theoretical for any non-trivial program anyway, and when you're using standard libraries, OS APIs, and code from who knows where you can forget about proving anything. Again, even without exceptions there's no guarantee that a function will return to its caller: it may simply crash. Or it may return an error code that's ignored or misinterpreted.

There's no requirement that code know about exceptions thrown by code "50 levels deep." Any bit of code can either handle exceptions or ignore them and let them propagate. In fact adding exception handling to code is much easier than adding error-code based handling because you don't have to write any error propagation yourself, and that's a lot of tricky code you won't have a chance to get wrong.

Dismissing this discussion as a religious debate is not fair: Joel wrote that exceptions are worse than gotos and then expressed his personal preference. I've read most of the followup comments and I don't think any of it has turned into a religious debate--in fact there have been lots of good points and ideas from both sides.

I will agree that threads make programming and reading programs harder. I've yet to find a use for them, but I'm sure there are valid applications. Whenever I see someone tinkering with threads (or more usually debugging threaded code) I ask them why they used threads. So far the answers have all been about coolness and imaginary optimizations, the hallmarks of the amateur.

Gregory Jorgensen
Wednesday, October 15, 2003

Threads are best used when you need to wait for something efficiently. I just recently did a simple library to receive messages off a socket. I put the socket receive call into another thread, because otherwise the main loop of the GUI app would be stuck waiting on the socket.

And I disagree that threading makes it impossible to prove correctness. Yes, threading in all its full memory-stomping glory, yes. But then again, so do global variables. You need to find a subset of threading that will get you what you need, and is provable.

For example, if all communication between threads went through a well-proven message queue system rather than by using global state, I would think that would be fairly easy to reason about.

A lot of this discussion reminds me of Cleanroom Software Engineering[1]. In this technique, you are explicitly forbidden from using constructs that you can't reason about locally. The theory being that if you never introduce something you can't prove correct, the whole program must be correct. Such techniques DO work, but the cost is high (in programmer morale if nothing else), and you have to really need the extra reliability.

-Chris

[1] http://www.cleansoft.com

Chris Tavares
Wednesday, October 15, 2003

Finally, a good thread... a few short points.

1. I didn't get the dismissal as a religious debate thing either. Usually when you say that they mean that people are just quoting some arbitrary authority, but most of the discussions have included real world benefits/problems borne out in practice.

It seems like Joel has backed up a bit too, saying there ARE in fact some good reasons to use exceptions. That would seem to contradict the policy of never throwing them and immediately catching any thrown by library calls.

2. It's good to see someone bring up provability. Especially since taking such care often isn't deemed worth it in most business settings. But, coming from a math background, this is pretty important to me, if only for peace of mind. The best thing about OOP is being able to establish class invariants, and thus hide a class's state when reasoning about the program. To me that has proved to be extremely powerful. But most people don't think this way instinctively, and haven't been trained to do so. I agree of course that complete provability is an unattainable goal, but the more classes/subsystems you have "proved", the smaller and more trivial your program becomes.

3. RE: Staring at code. While it is definitely nice to have your bugs in front of you, I have come to believe that reading a stream of a text is an extremely bad way for a human to comprehend a program. Code is "static", a running program is "dynamic". Code sort of represents space and spatial dependencies, but it poorly represents time and temporal dependencies. Unfortunately it is pretty much the only representation we have in practice, since pretty much nothing stays in sync with code, at least where I work.

Any time I write something non-trivial, there is some paper diagram that goes along with it, which gets lost soon after the code is written. Having to recreate this diagram, having never seen it, from code, is time-consuming and error-prone. Better to keep that high-level representation of the program, however rough it may be. Unfortunately, I haven't found/seen a good way to do that in a typical business environment.

In other words, I think a representation of a program should be compact, above all. Most programs "look" a lot more complicated than they actually are, IMO. So this kind of contradicts the principle that you should be able to determine all aspects of what a program is doing at a particular point in time from a particular block of code. To make a program compact, you must _necessarily_ store the details in other places. Because what's going on at one point in time *IS* complex, but typically there is a lot of redundancy that doesn't need to be expressed over and over in every block of code. Factoring out all this complexityy makes the program a lot easier to UNDERSTAND, if not to READ.

Perhaps another good example of this is Aspect-oriented programming (something I have not yet used much admittedly). I know Joel would REALLY dislike this, because you can insert code at join points in your functions, and it doesn't textually appear in line with the rest of the function's code -- the "flow". But this is another example "separation of concerns", which comes at the expense of readability. But to me readability ISN'T (or shouldn't be) that important, it is *comprehensibility* that counts (if that's a word).

Hope that last made sense, maybe someone can explain it better.

Roose
Wednesday, October 15, 2003

I was just thinking about the exception thing again. You know, one of the most powerful mathematical models for computation is the theory of partial functions. Modeling your code this way opens the way for very powerful tools to aid in "proving" or otherwise making inferences about the behavior of the code. This is especially useful in developing and working with complex algorithms - a situation in which the ability to draw inferences about the code is especially important.

It occurs to me that using return codes would, in general, compromise or at least complicate your ability to make use of these tools to reason about your code. Having explicit exceptions doesn't seem to be similarly disadvantaged, and it seems more natural since exceptions are properly outside the model (they represent limitations of the computing environment, not of the computation itself.)

Then again, it's late, and I might be crazy. Also, before I get dismissed as an ivory tower academic or something, let me just state for the record that I don't imagine that this kind of thing comes into play in everyday programming, or even that it should. I'm only thinking about the "provability" focus of this thread and how to think about the problem we're discussing.

DBC
Wednesday, October 15, 2003

It's true that you can't see which functions can throw exceptions from a code listing.

However, when developing in C#, Visual Studio .NET will quickly bring up a list of exceptions thrown by any function you care to point the mouse at.

James Taylor
Wednesday, October 15, 2003

Proofs should be done by code, like the xUnit testing frameworks or your homegrown. The VB6' Debug.Assert works just fine.

I don't understand why threads can't be prooved? The thread is executing some code, and if we can prove that code to be correct, then the thread has to be.

Thomas Eyde
Wednesday, October 15, 2003

"From my experience, programs designed with provability in mind, come out shorter, much more robust, much less buggy, and much simpler than when provability is not a design criterion. "

Of course. It is circular reasoning since any program that is beyond a simple small batch program would fail being provable. Unfortunatly outside of the CS curriculum we need programs that actually do "a lott of stuff", on the basis of vague domain models and requirements, in a messy environment that is poorly documented and on a limited budget.

P.S. Don't forget to prove your proves correctness.

Just me (Sir to you)
Wednesday, October 15, 2003

If your program needs the "many things going on at once" illusion, what will you do?
Maybe for small needs you can argue that writing your own dedicated code scheduler in a single thread will be simple. Let me guess: You'll start out with a "cooperative multitasking" type pattern?
When the complexity grows, you might want to make the transition to a decent thread library, no?

Just me (Sir to you)
Wednesday, October 15, 2003

When programming with synchronous exceptions, I expect Java to transform my code, writing code that I would've written anyway. If I evaluate a function, I assume it will return an object of type return-type + Throwable. I either deal with both explicitly (using a glorified if-else), and/or return that Throwable.

Finally blocks are similar transformations, to execute some side-effects.

This model has helped me write pretty decent code, and I think it's sound. Is there a hole in it? I'm not talking about asynch exceptions, which the standard promises only occur through internal errors or deprecated methods.

Tayssir John Gabbour
Wednesday, October 15, 2003

"ec = dosomething(a,b,c);
if (ec == 1)
// do something about error 1
else if (ec == 2)
// do something about error 2
...
"

This example given above is extremely bad programming practice. You should test for what you rely on, which - in this case, should be success. Not a specific set of error codes. You _might_ know what to do about a specific set, but basically, you should treat anything other than full success and things you exepct as failure. So it should read

else if (ec != 0) // 0 means success
// do something about unforeseen error.

This is equivalent to the cleanup you'll do in in catch-all or finally clause with exceptions.

I did address strict mathematical provability, dismissing it as incomplete at best because the tools are not provably correct in my 2nd post to this thread. But the fact that it doesn't give you 100% coverage is not reason enough to dismiss it, because NOTHING gives 100% coverage. The scope of proof you CAN give, does, however, provide significantly better coverage than any testing methodology can.

There was a question about "proving threads" earlier, which I feel the need to answer: The problem is not whether the thread is correct or not, but whether the program as a whole is correct or not. Let's go through the following example, which I made up, but is actually a simplified version of a bug I found in a financial piece of software that moves several millions of dollars from place to place each day.

Suppose you're writing a text editor, which does the real editing (keyboard input, buffer manipulation) in one thread, and saving in another (this can be reasonable if it's possible to make copy-on-write copies of a buffer). When the user presses 'Ctrl-S', the second thread is signaled to save the file, but it will only do so if the "file was modified" flag, which is set by buffer manipulation, is up.

Now comes joe user, who has the habbit to do 'one letter change' - 'save' - 'undo' in quick succession, and undo clears the "file modified bit" back to the last save. This pattern is common in some kind of files.

Joe comes and complains that files are not being saved every now and then. Odd, you think, because the code for save looks like this:

if (was_modified) {
say "I'm going to save"
}
for (i = 0; i < 10; ++i) {
do some other stuff, unconditional on whether changed or not.
}
if (was_modfiied) {
save_without_possibility_of_undetected_failure ()
}

So the only possible reason for this bug is that someone modified 'was_modified' behind your back.Who did? You'll have to scan a significant portion of your source code to prove that this is indeed the case, because if any thread may call any method on any object (as is often the case), then everything is suspect. Sure, you should have locks on everything, and no one should have changed was_modified in the background, but can you guarantee that without reviewing the code?

If you have just one instruction executing at any time, you can be sure that "if (was_modifed or not(was_modified))" is always true. With threads, you can't even reason about this ridiculous test without reviewing the rest of your code.

I've reviewed hundreds of programs. I can't recall a single instance that used threads in which a code review didn't uncover a race condition between the threads. In some cases, the race condition was semi-theoretical, in the sense that I couldn't devise a specific scenario that would make the problem behave badly, but neither was it possible to prove that it will behave well.

Just Me: This is not an academic exercise. If you can't reason with a good level of detail (down to specific variable values) that your program is behaving as it should, there are probably many cases that it doesn't. And if you consider qmail -- which, along with sendmail, is still responsible for the majority of mail transmission today -- a small batch file, then you're probably working on projects humble me cannot even begin to understand.

qmail was designed to be provably correct and provably secure. Of course, it does have to assume that the operating system is correct (and it does work around known bugs in imlpementations). It's definitely the fastest, least resource intensive mail server you can find. It has the shortest code of any, but it's still standard compliant to the letter.

qmail hasn't had a single security issue since publishing, and I'm not aware of any non-security bugs (although I'm sure there are a small number of insignificant ones). No other mail server, postfix included, has this track record. You may not like DJB's personal style, or his programming style -- neither is traditional in any sense -- yet, the code is short, provable, it works, and -- if you approach it with the "I want to learn" mindset rather than the "DJB sucks" mindset most people do, it's even readable. Different than anything you're used to, but readable.

Ori Berger
Wednesday, October 15, 2003

Chris and JustMe: About needing to use threads to avoid blocking, or "maintain the illusion" - in most cases, this is entirely unneeded.

Chris just mentioned that he uses threads not to block on network sockets. Sockets support asynchronous communications. You just flip a bit, and every socket call becomes non blocking. You use select() or WSAAsyncSelect() and the OS will alert your main loop whenever there's activity on the socket that you should check. You don't block for a keypress/mouseclick, and you shouldn't block for what is effectively a keypress except that it comes through a socket rather than your local keyboard.

JustMe: Cooperative threads are much better from a provability point of view, but they are usually an overkill. If you use Python, I'll point you to the excellent http://twistedmatrix.com framework - it's a main loop done right, that takes everything into account, including GUI, network, high level protocols, database access, and many other things.

Ask yourself, why is GUI different? Why is it that 99% of programs only have one main loop, and one thread to deal with GUI, no matter how many Windows I have open, or if I have a Find dialog or Wizard style dialog, which are basically sequential logic?

The answer is: GUI isn't different. And in fact, there were times when GUIs were done sequentially like it is common to do network programming today. But they sucked big time compared to event driven GUIs. And at the time, paradigms were evaluated based on merit rather than hype, so single threaded event driven GUIs took over.

I have the untestable hypothesis that if Microsoft integrated socket operations natively into the Windows message loop, that it would have been so perfectly clear to anyone. It would have been something like, you create a new "socket window", with HWND and all, for every connection, and then you'd get WM_INPUT_BLOCK, WM_CAN_OUTPUT_NOW, WM_CONNECT, and WM_CLOSE notifications that you would have had to deal with, just like you _have_ to deal with keypresses or mouse presses now.

GUI is not different. Only the mindset is.

Ori Berger
Wednesday, October 15, 2003

And ... to tie a few loose ends.

Joel: Thanks!

Mike and Anu: The halting problem says that you can't write a program that proves arbitrary programs correct or incorrect. But given a specific program at hand, it often can (and should!) be proved correct.

Mike: A relatively "provability-safe" way to use threads is to dedicate each thread to a _function_, not to an _input_ e.g., a thread that reads files from disks; a thread that does DNS lookups; A thread that does all network access except name lookups -- and NOT one thread for each connection. Communiacte between the main logic and the threads through message queues, not through global variables or function calls. There's a lot more to be told, and there are other "safe" ways, but, this one covers the majority of cases, and while this explanation is incomplete, it's in the general direction.

A "provability-safe" way to use exception is only for things that aren't supposed to be caught anywhere, or strictly with RIAA (but this is often impractical when interfacing with 3rd party products). Which makes exceptions not much more than a glorified "abort()" or "die()" call, and is why I don't recommend exceptions at all.

Ori Berger
Wednesday, October 15, 2003

Why should exceptions hurt provability? Part of the specification is what exceptions will or will not be handled. As long as the program properly handles what it says it can handle, and doesn't handle the rest, that should hurt provability no more than checking for error codes would.

T. Norman
Wednesday, October 15, 2003

Ori,

1. Provability: If I'm writing soemthing like a device driver, with well defined inputs, output and stimuli, then there really isn't any reason not to prove 100% correctness. In fact, if I haven't proved correctness prior to a large deployment, the large deployment will quickly prove me a poor programmer.

2. Having said that, I do not think that precludes threads, or that by using threads one cannot prove their work correct. The key is that:

a. All shared data be identified, and in turn all synchronization methods which "guard" shared data be identifed (mutexs, semaphores, conditionals, etc.).
b. All transactions which encounter sych methods be indentified.

And that's it. From these simple criteria, some other simple rules of thumb derive, most obviously: "global data is an abomination" because its impossible to identify all possible dependencies to that data without examining the entire code base.

In your example: "You just flip a bit, and every socket call becomes non blocking. You use select() and the OS will alert your main loop whenever there's activity on the socket that you should check."

Some thread is waiting on select, which is a blocking call. The thread waiting on select will wait either until something has happened on the file descriptor set or until the select times out. If your user presses a key, and your UI thread is waiting on select, that will make for a rather poor user experience.

Anyway, there are well known design rules for handling threads. These are the same basic rules for designing a re-entrant device driver:
1. Scrict scoping rules.
2. Limited and documented access to sychronization objects.

nat ersoz
Wednesday, October 15, 2003

Ok, I don't think Ori would mind me mentioning that we had a quick exchange and it became clear that a person who cares about correctness (read: program that works) would be interested in the advantages and disadvantages of different approaches. There are clear locality problems when you're loose with exceptions, and depending on the language and programmer, the tradeoffs become magnified.

Another point that occurs to me now is that exceptions may be superior in certain languages because they're very errcode-hostile. Further, a language like Java offers exceptions closer to the errcode mentality than C#'s, taking some ground that errcodes usually claim.

But ooh the power of exceptions. I suppose the point is to know exactly what the semantics of your constructs are, and not rely on vague philosophical arguments of ideals.

Tayssir John Gabbour
Wednesday, October 15, 2003

Ori,

My example was meant to illustrate my point, not to demonstrate good programming style. I deliberately wrote an example similar to the one Joel wrote to illustrate his preference for checking error codes. Obviously there are many ways to check the error codes. Again the point is that exceptions can completely simulate explicit error code checking, if that's how you want to write your code.

As for qmail, I've used it and I'll venture that it has two huge bugs: horrible documentation and an arrogant author. Asking for help with qmail often results in a harangue and aspersions on one's intelligence. It may be provably correct (I doubt it) and more secure than sendmail (I'm sure of it) but it's not useful if you cut your hands trying to use it.

Gregory Jorgensen
Wednesday, October 15, 2003

Ori,

We've already been down this path, and I've thought about your comments from the last time this topic came up.

You are correct that you can make socket servers single thread by using non blocking sockets and select() or similar to handle events as they occur, but you miss a couple points.

1) You do not take advantage of multiprocessor systems.

2) The state machines that are required to implement any non-trivial application protocol (such as HTTP 1.1 with chunked encoding), are more difficult to debug than the multithreaded code. They are certainly much more difficult to write. You might get a performance advantage from doing this, but it does not simplify the code. If the threads do not share data there will be MORE paths through the code as you transition between states. Even in simple scenarios were data needs to be locked I still feel the threaded solution will be far less complex. In my opinion you are trading one problem for another. I feel that the single threaded solution isn't chosen for code simplicity reasons, but for performance reasons.

3) Your solution relies more heavily on the OS TCP/IP stack to queue all in coming connections, which will likely take longer to be connected to a socket, as the main thread does nothing but sit in a tight loop calling accept() in a multithreaded solution.

Joel. Do you use ASP? Well hate to say it, but every request you handle is in a seperate thread. There is no way to avoid considering the implications of threading in most environments. Trust me if Microsoft implemented every request in a single thread using a state machine we'd be complaining about how ASP sucks.

I say avoid threading if possible, but it is the right solution in many cases. A solution that should be justified by the designer.

http://www.summitsage.com/

christopher baus (tahoe, nv)
Wednesday, October 15, 2003

Since we've gone down that path before, I'll just sum up my stance:

1) I'm not striving to use multiprocessor systems through threads, but rather through processes. I'll gladly debate this when I have time, but not now.

2) Look at TwistedMatrix. The HTTP server there is a good example. It's _not_ complicated compared to many other web servers. They wrote clients and servers for all protocols in common use, and they are all extremely simple from the provability point of view. Just read the code.

3) There is no main thread that tight-loops in accept(). There is (generally speaking) only one thread doing all network I/O, and it never busy waits for anything. If my loop uses 100% CPU on a single CPU machine then, most probably, my users will wait LESS on the average than users of a threaded server on the same machine, even though accept() will, on the average, be handled closer to the end of the 3-way handshake. Especially when you properly synchronize access, the overheads of synchronization are nonnegligible.

And Greg - about qmail - I didn't have any exchange with Dan myself, but I did have with others of the qmail community, and most of them are nice and helpful. I'm happy to see though, that you evaluate what "the best tool for the job" based on the manners of the developer. Do you use Microsoft software? They were found guilty of antitrust violations too, and you'd probably rank breaking the law worse than just being arrogant.

Many aspects of qmail's operations _have_ been proved correct. Not every single line of code; but privelege separation (which is a great concern in critical infrastructure) and other desirable properties have been proved.

Ori Berger
Wednesday, October 15, 2003

Ori,

There's no need to go down the path of making assumptions and ad hominem attacks. Reasonable people can disagree and argue without calling names.

"I'm happy to see though, that you evaluate what 'the best tool for the job' based on the manners of the developer."

That isn't what I wrote. The poor documentation and bad attitude of DJB did push me (and many other people) to Postfix, which is easier to set up, better documented, more secure than sendmail (and I'm sure less secure than qmail), and doesn't suffer under the weight of one huge ego. No doubt DJB is a lot smarter than I am when it comes to mail servers and secure software, maybe I'm just not getting it.

"Do you use Microsoft software? They were found guilty of antitrust violations too, and you'd probably rank breaking the law worse than just being arrogant."

Where did that red herring come from? Let's stick to the discussion at hand and not try to psychoanalyze each other, OK?

"Many aspects of qmail's operations _have_ been proved correct. Not every single line of code; but privelege separation (which is a great concern in critical infrastructure) and other desirable properties have been proved."

Great. Like I said the problem I had with qmail (and I know I'm not the only one) is the poor documentation and DJB's attitude. Whether the software is provably correct in any sense did not enter into the decision because getting it to run at all is too much trouble. Your mileage may vary. My ISP (Pair Networks) uses qmail and other than its arms-length interface to procmail I have no problem with it because I don't have to install or manage it.

Gregory Jorgensen
Wednesday, October 15, 2003

Regard my comment regarding the tight loop...

What I meant is in a multi-threaded (MT) solution there is typically one thread which sits on accept() and sets up the connections (and spawns worker threads). This should reduce the number of unconnected sockets in the incoming TCP/IP stack over the single threaded (ST) implemenation which can not set up a new connection while it is handling another.

Having written an HTTP 1.1 implementation from the ground up, I am interested in any examples that are ST and simplier than my implementation. I tried to convert the code to ST, but realized it made it much more complicated. I still want to do it for performance reasons, but I don't think it will end up simpler..

christopher baus (tahoe, nv)
Thursday, October 16, 2003

An example of the complications that arise parsing HTTP in a single thread...

Let's say you are parsing the following:

accept: img/jpg

Now lets say that at the first g, all the data has been read from the socket, so the server must create a pointer and the state information which will allow it to return to parsing the field value and associate that information with the socket handle.

Upon returning to select() the server retrieves data for a completly different connection and pulls the state information associated with the socket, and continue parsing where this second connection had previously left off.

In HTTP there are hundreds of different ways you could continue parsing and in a single threaded implementation you'd have to be prepared to return to any of them.

This is difficult to do correctly. It is far more difficult than using threads which maintain all the state information for you conveniently in the call stack.

The only example you can point to is some obscure Python implementation. Do you know anyone who uses the server in production? I know of one production quality HTTP server that is single threaded and that is Zeus. I suspect they didn't design it as single threaded for ease of development, but for raw performance.

christopher baus (tahoe, nv)
Thursday, October 16, 2003

Christopher, I know _many_ systems that use it, but unfortunately, I can't point you to closed source systems.

TwistedMatrix, while not hugely popular, has many many users. The reason I am pointing towards it is that (a) it's single threaded; (b) it's open source; (c) it integrates GUI and database access into the same framework, which is something that all single threading opponents keep bringing up as 'impossible'. (d) it's well designed and well implemented. Not perfect, but very good indeed. (e) it's well documented. They have good examples about how to add your own protocols, and you can always look at how they implemented the standard protocols. If you read the sources, you'll notice that everything about thread switching is implicit.

qmail's send engine is single threaded; but I don't refer anyone to it unless they're really interested because it takes time to grok (not the logic; Dan's coding style). kdb, a superfast relational database is single threaded (although multiprocess, in order to break the 2GB/process limit), but it isn't open source.

And I _did_ point you at the perfect analogy - GUI. Which I'll expand:
A new conncetion <-> opening a new window
keypress/mousepress <-> character available at the socket
pressing "enter" at the end of the input field <-> The \r\n at the end of a line
pressing "Next" at the bottom of the wizard window <-> The \r\n\r\n that separates header from data in the connection.

99% of GUI programs not written in Java are single threaded. VB, for example, _had_ no other way. And it works perfectly. If you can't point to a flaw in this analogy on one hand, and can't see what the conclusion on the other, than I don't think I know how to explain better.

Gregory: I apologize. I read your original post as "qmail sucks because its author is arrogant", which, I think, is not an unreasonable interpretation, but apparently not what you meant. No offence intended.

nat: On Unix, you can select() on GUI input just as well as socket input; and on Windows, you can get your main loop to wake up whenever there's socket activity just as well as GUI activity. If you are not familiar, read on WSAAsyncSelect() on Windows. I don't recall the X-Windows equivalent, but if you're really interested, I can look it up for you.

Does the GUI analogy have a SEP field on it? It's either flawed, in which case someone should be able to point out the flaw, or correct, in which case there's no point arguing about network independently.

Ori Berger
Thursday, October 16, 2003

Ori,

>> There is a school of thought in programming, which I belong to, and few others do, that hold to the ridiculous idea that you should be able to prove your program correct. That does not mean you actually have to prove your program correct every time - it does mean that you should be able to, when the need arrives.
And "proof" here is in the mathematical sense, that which does not depend on opinion or hype - a correct proof is irrefutable. <<

I get the impression that you're either quite new to software development or rather naive about the subject.

I'm also unclear about your understanding of "mathematical proof". For example, in the logicist formalization of mathematics, paradoxes such as Russell's paradox arise. Russell's paradox is the set of all sets which do not contain themselves. Therefore, the set is a member of itself if and only if it is not a member of itself.

Russell and Whitehead, in an effort to avoid paradoxes, used the theory of types, the axiom of reducibility, the axiom of infinity, and the axiom of choice. The primary criticism of the axioms of reducibility, infinity, and choice is that they are not axioms of logic at all, negating Russell and Whitehead's claim to the derivation of mathematics from logic.

In 1931, with his paper "On Formally Undecidable Propositions of Principia Mathematica and Related Systems", Kurt Gödel proved the impossibility of the formalist and logicist attempts to axiomatize all of mathematics. Known as Gödel's Incompleteness Theorem, the paper shows that in any logical system using symbols, it is possible "to construct an axiom that is neither provable nor disprovable within the same system". This undecidable nature means that any system that encompasses the theory of whole numbers and is consistent will not be complete.

Do the mathematical "proofs" of your programs take account of this? How do you perform these mathematical proofs?

Totally apart from your interesting use of the term "mathematical proof", showing that your program is correct is useless in the real world. The only useful way forward is to show that the system that includes your program is operating correctly. This includes:

The hardware.
The network protocols.
The microcode.
The firmware
The OS.
Your language compiler.
Your language code libraries.
Your 3rd-party code libraries.
Your application code.
Code in other apps running with your app.

And on and on and on....

If you tell your end-users that your app is provably correct and therefore the problem must lie elsewhere (perhaps cosmic rays affecting the hardware?), you're not going to be in business for very long.

Mark
----
Author of "Comprehensive VB .NET Debugging"
http://www.apress.com/book/bookDisplay.html?bID=128

Mark Pearce
Thursday, October 16, 2003

Mark, I'm not new to programming.

Goedel's theorem has nothing to do with whether a specific program is provably correct or not (neither does the halting problem, which is just as irrelevent, but was raised earlier).

I don't tell my users my app is provably correct, because (and if you bothered to read the thread you'd have noticed), I rarely try to prove my app correct.

But I have been delivering commercial software for a variety of processors, operating systems, and uses - shrink wrap, enterprise, financial, device drivers, frameworks, mathematical, you name it - for the last 16 years; And I've been doing it with a low bug rate that most people I've worked with over the years found somewhere between unbelivable and impossible.

Apparently, we live in separate worlds. I have no problem that no one bothers to look through the SEP field - As long as it's this way, it's guaranteed that I can be competive with any outsourced project that uses the inefficient approach.

Ori Berger
Thursday, October 16, 2003

Ori,

First, my apologies for being quite wrong about your level of experience.

>> Goedel's theorem has nothing to do with whether a specific program is provably correct or not (neither does the halting problem, which is just as irrelevent, but was raised earlier). <<

I agree about the irrelevance of the halting problem, but Godel's Theorem does indeed apply. In order to get a mathematically correct proof, you need to convert your logic into a mathematical form - that's when the problems that I mentioned arise. I always squirm when developers talk about a "mathematical proof".

Perhaps you didn't really mean a mathematical proof, but some sort of logical proof?

>> I don't tell my users my app is provably correct, because (and if you bothered to read the thread you'd have noticed), I rarely try to prove my app correct. <<

Yes, I did understand this point. What I don't understand is how you can ever manage to prove that your app is correct. First, do you mean "your app" or the complete system in which your app resides? Second, how do you go about performing any proof of a complex program in the real world (outside of academia, which only deals with trivial program proofs).

>> And I've been doing it with a low bug rate that most people I've worked with over the years found somewhere between unbelivable and impossible. <<

I can believe this, as I've seen this done by a few other developers. Bear in mind that this says as much about the people you work with as your own ability :)

I've never seen this ability to produce low-defect code related to any type of program proof. If anything, this ability seems to be related to an innate ability to design good systems. In my experience, the system and low-level design stages have a huge effect on the amount of implementation bugs, far more so than, say, my ability to write good code.

Mark

Mark Pearce
Thursday, October 16, 2003

I used the term "proof in the mathematical sense" and contrasted it was "proof in the legal sense". I'm not aware of a fine distinction between a "mathematical proof" and a "logical proof" that you are referring to. English is not my mother tongue, and as all my studied were done in Hebrew, I may have missed this fine distinction.

I mean proof at the same level as one usually does in e.g., high school classes. Not down to Goedel encoding or axiomatic formulations of number theory, as is required for general theories; Rather, the level of proof that is usually used to become convinced in truths such as the Pythagorean theorem (in a right-angled triangle, c^2=a^2+b^2). (c being the hypotenus (sp?))

There is an elegant proof for this theorem, that relies on a+b=b+a, and on the fact the area of right-angled triangle is (a*b)/2.

The proof is incomplete in the sense that it does not assert that a+b=b+a; Neither does it assert the area to be (a*b)/2. Proof for the latter can trivially be incorporated into the elegant proof. Proof of the former is extremely hard (in fact, it does not even follow from Peano's axioms, and is a fine example of an everyday encountered incompleteness).

To complete this proof, you have to add a model for numbers that underly the Peano axioms, and proof a+b=b+a follows in that model (or go farther and prove that a+b=b+a in every model in which the Peano axioms hold true).

Nevertheless, the simple, elegant, incomplete proof is sufficient for 99.9999% of uses, 99.9999% of the time, to be sure of Pythagoras' theorem.

I strive for the same level of provability. It isn't constructive to require proofs for a+b=b+a, or proof that the compiler generates correct code, or even that the processor correctly processes machine language - they are tedious, and generally get you as the app developer nowhere.

However, once you state your "axioms" like: a+b=b+a, or "the compiler generates correct code", you _can_ prove correctness, even for large apps (if they are well modularized, and you can prove each module separately and then their interaction).

Just recently, I've discovered a bug in VC6's treatment of float<->double conversion. It took me 10 minutes from the time the user reported the bug - what he reported was easy to prove impossible (in the "elegant proof" sense), yet it did happen. The conclusion was that my axioms were wrong. Looking at the generated assembly code revealed that the compiler optimized something it shouldn't (and that was a Debug build).

If the code wasn't built with proof in mind, I probably would have chased that for days. But the code WAS built with proof in mind, and even though I never tried to prove it correct before, it took me all of 4 minutes to be convinced that the bug was most probably is in the compiler, and not even with a library I was using. If the code was wrong, then I (or someone else) trying to prove it right would probably have found the bug.

And - about bug free code - my experience relates simplicity with low defect rate. provability is a good measure for simplicity, I think, because - as others have pointed numerous times - when a system becomes complex, you can't really reason about it in any meaningful way.

And some things just can't be made simple - but an overwhelming majority of things _can_ be made simple, and unfortunately aren't.

Ori Berger
Thursday, October 16, 2003

When I say an example, I mean an HTTP 1.1 example since that is the protocol I care about. Add something like soap to the message body and I think you are asking for a nightmare ST solution. It certainly would be easier to write a ST server if I could control the protocol. But I can't. IIS is multithread, Apache is multithread/multiprocessed,the old Netscape server is multithreaded. I just don't really know of a single threaded server other than Zeus. I still think writing a ST HTTP server is Hard (tm) and equally, if not more, error prone as the MT server. Not to say it is impossible, just you have to be sure you know why you've choosen such an adventure.

http://www.summitsage.com/

christopher baus www.summitsage.com
Thursday, October 16, 2003

Ori,

>> I used the term "proof in the mathematical sense" and contrasted it was "proof in the legal sense". I'm not aware of a fine distinction between a "mathematical proof" and a "logical proof" that you are referring to. <<

Now I understand what the misunderstanding arose. Yes indeed, there is a huge distinction between the two types of proof, and you are referring to the logical proof of your program.

>> However, once you state your "axioms" like: a+b=b+a, or "the compiler generates correct code", you _can_ prove correctness, even for large apps (if they are well modularized, and you can prove each module separately and then their interaction). <<

I just don't believe that you can provide this proof. Having written a book on debugging, and co-authored two other books on the same subject, I've never come across any developer who can provide logical program proofs for non-trivial programs. Maybe I've just lived a sheltered life.

How do you go about proving your program? No code inspection can provide a decent proof. No execution testing can provide this proof. So exactly how do you do it?

Here's an example. How would you go about proving the correctness or in-correctness of this semantically-simple C# code snippet?

using System;
using System.Runtime.InteropServices;

public class Quiz
{
const int E_NOINTERFACE = unchecked((int)
0x80004002);
const int E_POINTER = unchecked((int)
0x80004003);

public static void Main ()
{

try
{
Marshal.ThrowExceptionForHR
(E_NOINTERFACE);
}
catch (Exception ex)
{
Console.WriteLine("0x{0:x}",
Marshal.GetHRForException(ex));
}

try
{
Marshal.ThrowExceptionForHR(E_POINTER);
}
catch (Exception ex)
{
Console.WriteLine("0x{0:x}",
Marshal.GetHRForException(ex));
}
}
}

If you think this code is easy to prove, try to run it and then explain the results you see. Don't be surprised if you find the results hard to explain :)

Maybe the code in that quiz was too complex. If so, here's an even more semantically-simple C# code snippet for you to prove is correct or incorrect:

public static void Main ()
{
// Open the registry key for read-only access
RegistryKey key =
Registry.LocalMachine.OpenSubKey(
"Software\\Microsoft\\.NETFramework");
Console.WriteLine("Install root: " +
key.GetValue("InstallRoot"));
}

I'll give you a clue - this code has one major bug. If you want another clue, it can also trigger another major bug. So how would you provide a proof that this code is incorrect?

I can provide literally dozens of examples like this, many of them much more baroque and bizarre. And this is just a few lines of code, not a whole system.

Mark

Mark Pearce
Thursday, October 16, 2003

Mark,

First of all, I haven't yet started looking at C#, so I won't venture proofs regarding C# or the CLR. A proof requires axioms, and I don't have my C#/CLR axioms in place yet.

That said, I'm sure you can provide dozens of examples like this (after Adam Nathan posts them, that is; If you're not original, at least give credit where credit is due).

Furthremore, as opposed to Adam who stated the problem _clearly_, you didn't define what it is that the programs are expected to do. The way you stated your problem, it's possible that the programs behave correctly - for all I know, perhaps they _should_ have been giving this output.

But, for the benefit of other readers, who may have been stretching their minds, I'll say that the first example wouldn't give the expected result (if you knew what to expect ...) because of intricate implementation details of the GetHRForException method, which I couldn't find anywhere in the MSDN, but which Adam explains.

As I said, I'm don't do C#/CLR, and I may have missed something or looked for the wrong things, but I can't find a description of the mechanics of these calls in the MSDN, or, for that matter, anywhere else on the net -- except Adam's blog.

The second problem exposes what can probably be considered a bug in the RegistryKey implementation, and Adam claims it will be fixed in the next major .NET release. This specific problem _can_ be solved, though, by properly close()ing the key.

Both problems have to do with the ill-specified behaviour of transition between managed and unmanaged code.

Whether you're aware of it or not, you're using the axioms that the documentation is correct and mostly complete. Both these cases resolve around these axioms being wrong. Obviously, one can't reason much with wrong axioms. I didn't think I needed to state this.

I _can_ prove things with documentation I can trust, though; So, Mark, can you possibly look up a Quiz at Adam's site that includes Unix APIs, ANSI C APIs or Win32 APIs?

Thanks.

Ori Berger
Thursday, October 16, 2003

Ori,

maybe if you give us an example of some code and your correctness prove for it we can get a clearer picture of exactly what you are talking about.

Just me (Sir to you)
Friday, October 17, 2003

Ori,

>> A proof requires axioms, and I don't have my C#/CLR axioms in place yet. <<

You seem to be retreating more and more into a corner, putting ever more difficult and strange constraints on your ability to provide logical proofs. If your logical proofs require (amongst other things) correct and complete .NET documentation, then you will never be able to provide proofs for your .NET programs.

>> That said, I'm sure you can provide dozens of examples like this (after Adam Nathan posts them, that is; If you're not original, at least give credit where credit is due). <<

If you want some original examples, you'll need to buy my recent book :). I'm sorry, but nobody pays me to build and test original examples for you. And if I had given credit to Adam, that would have simply given away the answers to my quizzes.

>> The way you stated your problem, it's possible that the programs behave correctly - for all I know, perhaps they _should_ have been giving this output. <<

What these code snipets are designed to do is obvious to anybody who does C# and .NET development. Can you only generate your program proofs with a requirements spec that documents every line of code?

>> Both problems have to do with the ill-specified behaviour of transition between managed and unmanaged code. <<

All, and I repeat all, software is prone to ill-specified behaviour. If your logical proof relies on well-specified behaviour, then it's effectively useless in the real world.

>> Whether you're aware of it or not, you're using the axioms that the documentation is correct and mostly complete. Both these cases resolve around these axioms being wrong. Obviously, one can't reason much with wrong axioms. <<

It's you that's using and relying on these axioms, not me. Once again, if you rely on the fact that any documentation is both correct and complete for your program proofs, then they're completely useless in the real world.

The main point of documentation is often specifically NOT to be complete and correct. That level of detail would just overwhelm the reader. If you don't believe this, try reading Chris Brumme's blog for some insight into just how hairy even a moderate level of detail can be.
http://blogs.gotdotnet.com/cbrumme/

Mark

Mark Pearce
Friday, October 17, 2003

For those interested in the first quiz, here's the discussion hosted by Adam Nathan:
http://tinyurl.com/r9kg

For those interested in the second quiz, here's the discussion hosted by Adam Nathan:
http://tinyurl.com/r9kh

For more of these quizzes, see Adam Nathan's blog:
http://blogs.gotdotnet.com/anathan/

Mark

Mark Pearce
Friday, October 17, 2003

All the reason not to use .NET then, or at the very least the interoperability stuff. Documentation should be reasonably complete, and reasonably correct. In the first example, there is a stateful caching behaviour not described _anywhere_, that makes the HR stuff not behave according to the docs.

If you want me to prove C#/CLR programs, you'll have to pay ME. I use tools that I _can_ rely on, resulting in programs that _can_ be reasoned about, usually shorter and more robust. Your apparent religious assumption that one should adopt new 'technologies' (for whatever reason) isn't too reasonable based on collective real world experience.

Yes, I have less tools at my disposable than someone who does adopt everything new - but these are tools are reliable, well documetned, and _do_ cover what I need.

If you stumbled upon the RegistryKey problems you listed above, you'd probably look at them for hours, or worse: You'd not notice them in your testing, ship them, and your clients will (just one out of 50, and in a completely non-reproducible fashion).

Whereas I'd be writing it in C, single threaded and all, and have almost no such problems. If a client of mine demanded I used .NET, I'd respectfully refuse, and tell him I'll gladly do the project in 5 years or so, when the boundary conditions are better understood and ironed out.

It's not that, e.g., the Win32 documentation is perfect; I gave, in the beginning, the example that DeleteFile() does not necessarily delete the file, despite returning success. It's not documented anywhere I'm aware of.

But most Win32 issues have been ironed out and are well documented. Enjoy debugging both CLR code, which you have no control over, and your own code. I'll stay with debugging my code.

"First mover advantage" rarely exists in the business world, and never exists in a choice of programming languages. If you believe otherwise, you should study your history.

There's a wonderful quote from the Python mailing list of a while ago:
"There is a certain charm to seeing someone happily advocate a triangular wheel because it has one less bump per revolution than a square wheel does."—Chuck Swiger

The "wheel" here is provable deterministic program execution. Excuse me if I wait till the edges of .NET are sanded till the bumps are not as hard.

Ori Berger
Friday, October 17, 2003

Ori,

Your definition of logical proof seems to involve the mental examination of your code in the context of correct and complete documentation, correct and complete requirements, great familiarity with your programming tools and libraries, and an absolute avoidance of "complex" code such as multithreading and exceptions.

Is this a fair summation of your position?

Well, I live back here on planet Earth. I don't have complete knowledge of, or complete trust in, any aspect of my development environment. And above all, I don't deceive myself about my ability to verify code.

I come from the world of professional chess, where any player's belief in his own intellect, judgement and imagination is subject to frequent violent reversals at the hands of other players. THis has given me a strong sense of my own intellectual frailities.

And I'm sure that you'll forgive me if that means I flat-out don't believe a developer like you who claims their code is provably correct.

Mark

Mark Pearce
Friday, October 17, 2003

Let's agree to disagree here, as I think we've been adding nothing new in the last few posts, and it's obvious neither of us is getting convinced of anything the other claims.

Your summation is close, but not right:
I require _reasonably_ correct documentation (that is, a negligably small number of incorrect statements in the documentation), which is reasonably complete (that is, make a mention of things that could alter behaviour such as statefulness).

I do not require correct or complete requirements, but I _do_ require a reasonably well defined requirement when faced with a bug. Because one man's bug is a feature to another, and a third is agnostic to that issue.

Great familiarity with programming tools is a necessity, yes. I dare say that the probability for delivering a robust solution without being well aware of the possibilities and limitations of your toolset are slim to none. Would you play against another master who's famous for his sicillian without good knowledge of the sicillian variant he's fond of?

And yes, I advocate avoidance as much as possible (which is far from absolute) of constructs like threads and exceptions, as more often than not I can do without their complexity.

"reasonable" is not well defined, of course - engineering is, among other things, the art of compromise.

I don't believe in anyone's ability to verify large amounts of code, but verifying small sections is more than possible - it's often a necessity. I strive to make as large sections as possible of my code verifyable.

And I certainly don't believe in my ability to verify code that was not written with verification in mind.

I come from the world of professional software. I'm well aware of my frailities, which is why I am very picky about the tools I use. Unlike most people around here, a rounding error or race condition in code I write can potentially cost millions of dollars, easily a few thousands. I don't want to come to my coworkers saying "gee, well, it looks like the overzealous garbage collector combined with a bug in the Registry implementation is to blame for this quarters' results", however true it may be.

You probably wouldn't bet real money on yourself being able to beat Kasparov, even though you'd love the mental exercise. But you'd probably feel good enough to bet real money on winning against someone you've played 1000 games with, and won 995 of, even though you'd find this intellectually boring - especially if you had 1000 games to play.

Professionally, I pick the latter, every time. And I have found out that the techniques I use to achieve that do not actually cost me an arm and a leg - they take little more at first, and then quickly pay off in debugging and troubleshooting time. I can't eliminate uncertainty, but I can minimize it.

But I obviously can't convince you of that; And I don't seem to be convinced by any of your arguments that I _must_ deal with so much uncertainty.

So let's just peacefully agree to disagree, and leave it at that.

Ori Berger
Friday, October 17, 2003

Ori,

>> Great familiarity with programming tools is a necessity, yes. I dare say that the probability for delivering a robust solution without being well aware of the possibilities and limitations of your toolset are slim to none. Would you play against another master who's famous for his sicillian without good knowledge of the sicillian variant he's fond of? <<

This is actually quite an interesting analogy. Yes, I would prepare for my opponent by examining his published games. But what happens in reality is that after preliminary skirmishes looking for familiar ground, both players usualy end up on more or less unfamiliar ground.

And this is also what happens in most programming environments, which makes the concept of logical proofs totally alien to me.

As you say, let's agree to disagree.

Mark

Mark Pearce
Friday, October 17, 2003