I don't have high hopes about the possibility of perfectly bug-free software. To be bug-free from an end-user's standpoint, it seems like such a thing would nee

I don't have high hopes about the possibility of perfectly bug-free software. To be bug-free from an end-user's standpoint, it seems like such a thing would need to be completely free of errors at every level, from specification (understanding precisely what the program is supposed to do, whether in terms of problem domain or customers' requests) to implementation (the bug-free program itself) to the supporting system and hardware (an otherwise perfect program could still fail due to a bug in a floating point processor, for example). Each layer presents its own problems, many of which are far from trivial. Perhaps a more useful way to frame the question is to ask what approaches could better rule out different kinds of bugs. For example, the strong type system in ML languages (e.g. OCaml) is great for preventing bugs with extensive compile-time analysis (in part due to being derived from a theorem prover), but there is certainly room for improvement. Likewise, well-designed garbage collectors can rule out many kinds of memory leaks.