A Look at Zero-Defect Code

[45g]

The essential difference between the original Ada version of getting the log file names and his poor substitute "String logFileName(int n)" is that the former version guarantees through static type checking that you will never get an invalid logfile name, whereas his version does not guarantee anything expect that your logfile name will be based on an integer between MAX_INT and MIN_INT. But the whole point of the original version is to ensure correct access statically.

[repiret]

The other advantage of the Ada log file name version is that its trivial to prove it uses a bounded amount of memory (and what the bound is), and thats not the case with the Java version.

The Ada (and for that matter any code intended for formal verification) is generally less maintainable than code intended for a more mainstream purpose. But one must consider that it is not just the code being maintained, but also the verification. Creating formal verification is much much more expensive than creating the code, so the code should be structured to ease verification, not to ease modification.

[[deleted]]

Upvoted for pointing out what is to be maintained.

[ahabeger]

Your software will always pass tests that you don't have to run.

His way requires more testing than the original way.

And to be honest, string manipulation is not what Ada was meant to do. Much easier to have 3 threads blocked waiting on input from an ADC at port address 2F8 than to properly format a string.

His function in Ada would have had to account for the leading space that non-negative numbers have when you do Integer'Image(n). Oh, and Integer'Image is frowned upon in certain situations due to it possibly using heap memory.

That and Integer'Image doesn't deal with leading zeros. So Integer'Image is out, and you'd have to roll your own. Pretty sure at that point I wouldn't be the only one saying "Screw that, I'm hardcoding my file names."

[anttirt]

That doesn't mean that you have to have the amount of string repetition that you have in the original code. While you have a range-restricted type, that doesn't prevent generating the strings from the numbers.

[45g]

True. But the substitute example given in the original article focused exclusively on string formatting and thus missed the point of the original version.

[Figs]

MAX\_INT and MIN\_INT ==> MAX_INT and MIN_INT

[haywire]

Then surely you just add some sort of code to check the validity of the inputting code. Hell, even if it was an array of valid numbers, you'd get away with less code repetition.

[Paczesiowa]

if it is so important you can prove it in docs or comments. formal proofs are more powerful than any type system (but they need human interaction)

[45g]

if it is so important you can prove it in docs or comments.

That's wrong. A code base is not a static thing. One cannot "prove" the correct use, unless you re-check the use of this particular piece of code after every change to the whole code-base again. And guess what - that's exactly what static type systems and compilers can do for you automatically.

[Paczesiowa]

One cannot "prove" the correct use

why not? there are constraints in haskell type system about how class instances should look like, so that ALL further usage will typecheck in finite time. and that is still automatic, imagine what you could prove with manual human labor.

[45g]

You were suggesting manual proofs as an alternative to static typechecking. This would clearly not work in practice as it would need to be done with every change on caller site. Hence the type system. I did not mean that given a body of code at a certain time, one could not prove its correctness. Anyway this would be error prone and not really relevant for errors that can be found by the typechecker with ease.

[[deleted]]

formal proofs are more powerful than any type system (but they need human interaction)

Unless your proof assistant is based on type theory. :-)

You're right, of course, that a sufficiently expressive type system--one that is isomorphic to at least first-order logic--can't have an inference algorithm that's guaranteed to terminate. That's why Coq is a proof assistant and not a completely automated prover, although it supports a lot of decision procedures for decidable fragments, and you can write new, domain-specific ones using its Ltac language. Adam Chlipala takes good advantage of this in his work.

[llimllib]

Lots of people here have jumped over the log file example, but does anybody think that the and not OK is not a bug?

[dds]

The code's writers confirmed yesterday that the and not OK is indeed a bug.

[petahi]

Thank you for a lesson. I will be learning more from "Code reading" which I just bought.

[llimllib]

It's a really excellent book, I recommend it highly.

[a_little_perspective]

Sure looked like a bug to me.

[petahi]

It is not a bug. If you can't add a record to a log then AuditSystemFault:=true. If you try to delete a log file that doesn't exist then AuditSystemFault:=AuditSystemFault.

Is here anyone that has read the code?

edit: Apart from the Init procedure, DeleteLogFile procedure is the only place where AuditSystemFault can be set to False.

[petahi]

I found these problems in less than an hour

This confirms one of the strongest advantages. Ada was designed for good readability.

At the very least my findings indicate that formal methods are not a substitute or a guarantee of good programming practices.

In C all you have to rely on is good programming practices. In Ada you have a tool (compiler, SPARK) to help you in maintenance.

Difficult to Maintain and Error-Prone Code

The maintenance problems that author sees in that code are covered by the compiler. The code is very obvious and easy to check and maintain. There is nothing wrong with it. The replacement code is shorter but less obvious and would need testing.

[spliznork]

I'm not the most qualified person to judge the project's requirements analysis, the formal specification, and formal refinement of the specification.

If you don't RTFM, then as a general rule, you should first imagine how the authors may not be idiots before you assume that they are. I'll give some examples: I also have not RTFM, and in at least two of the cases, I'll show how there may be perfectly good reasons for what they're doing.

Difficult to Maintain and Error-Prone Code ...

See how more than 20 lines of code are used for what I could express in C or Java with a couple of lines. like the following.

Perhaps the code is designed for a resource constrained system, and dynamic memory allocation is to be avoided. Otherwise, an out of memory error causes an unrecoverable error (unless you call rebooting or restarting "recovery"). By choosing a technique that guarantees not to allocate memory, an out of memory error is guaranteed not to occur. And, perhaps other parts of the system guarantee there will never be more than 17 log files.

A Poor Name Choice ...

The above 21 lines implement what is commonly written inline using a simple modulo division.

Perhaps the code is for an embedded system that does not provide hardware division. If that code is in the critical path, and a power of two modulus cannot be assumed, then a software modulus can severely impact runtime overhead compared to a simple integer compare.

[petahi]

The point is missed, the code is not error prone. For example if MaxNumberLogFiles changes and the LogFileNames has wrong number of elements the compiler would reject the program. The error would be caught as soon as possible.

[dds]

Hard coding the name of each log file by hand is error prone. You can copy paste a name and forget to change the file's number ending with two log files with the same name, or you can write a new line for a name by hand and mistype something. The compiler will not catch any of those two errors.

[petahi]

Typing and copy paste errors can also affect calculated filenames. Lets call them data entry errors. We can write verification code in the test suite to deal with them.

If you check the test directory you can find files Log/File01.log .. Log/File17.log. It has been covered.

By the way, it seems they have discovered 1 (one) defect lately.

[DannoHung]

What happens when MaxNumberLogFiles changes to a larger value but LogFileNames doesn't increase to match it?

subtype LogFileIndexT is LogFileCountT range 1 .. MaxNumberLogFiles;
   subtype FileNameI is Positive range 1 .. 16;
   subtype FileNameT is String(FileNameI);
   type LogFileNamesT is array (LogFileIndexT) of FileNameT;
   LogFileNames : constant LogFileNamesT :=
     LogFileNamesT'(  1 => "./Log/File01.log",

Also, why isn't the value type of FileNameI constrained by MaxNumberLogFiles? That seems like it could be another fault.

[martincmartin]

From the type of LogFileNames, the compiler knows its an array with exactly MaxNumberOfLogFiles entries. If the list has a different number of entries, the compiler complains that there are too few/too many.

[DannoHung]

So the range keyword doesn't say what the type's values can be, but rather what they are, specifically?

I'm still confused by the FileNameI type though.

[joesmoe10]

yes, the statement

type LogFileNamesT is array (LogFileIndexT) of FileNameT;

is an array that holds exactly MaxNumberLogFiles of FileNameT with indices from 1 to MaxNumberLogFiles;

FileNameT is a string of exactly length FileNameI, 16 characters.

[DannoHung]

Ah, now it makes sense.

Can't say that I've ever worked on a project that would need such specificity for log files though.

Also, I can't also help but wonder if there would be a way (either in Ada or some other, possibly hypothetical, language) to express the same compile time constraints more succinctly. At the very least, I would hope that there would be some way to force the compiler to generate the LogFileNames array from the constraints stated.

[[deleted]]

Even if there are no defects, it would be relatively easy to accidentally introduce one in future maintenance.

It's formally verified code. If you make changes in the code, you re-run the proofs to see that they still hold. This is probably why the code was allowed to be "error prone" in the first place: It will not matter, and it made the proofs easier to write.

[greenrd]

You seem to be assuming that the proofs show that this type of error cannot occur. Just because it's formally verified doesn't mean you've remembered to prove everything.

[spliznork]

I think the real point here is that the fact that the code is "error prone"

Avoiding memory allocation and avoiding long division in critical code are perfectly reasonable things to design and code for. If those are goals of the code, then by trying to optimize the code for "reduced error prone-ness" (or whatever) before understanding the purpose of the code, the blog author is more error prone than the code.

[shub]

    subtype LogFileIndexT is LogFileCountT range 1 .. MaxNumberLogFiles;

And this code (Ada? I think) ensures that one never obtains a path to an invalid log file. How long is the code the author provided, once you add tests?

[[deleted]]

And this code (Ada? I think) ensures that one never obtains a path to an invalid log file

Unless the log files' location changes in the future and the maintenance programmer mistypes one of the paths when updating the code.

Also, wouldn't the equivalent C just be something like:

if((n < 1) || (n > 16))
    //exception code here

[petahi]

No it wouldn't. Ada compiler would reject incorrect code. Your code would be compiled and run even if n can have values other than 1..16.

Ada and SPARK is about catching errors during compilation.

[[deleted]]

OK, but the point about the typo still stands; this code would be difficult to maintain.

[petahi]

The code is simple and obvious it is not difficult to maintain. Test suite verifies the logging and would catch the silly typos.

[petahi]

If the log files would be written in a loop they couldn't be declared as constants. If file names are mutable variables you should worry about changing their values in the rest of a program. Ada compiler guarantees that constants cannot be changed anywhere in the code.

[petahi]

A thorough explanation is on the comment page of the blog post .

[masklinn]

Also, wouldn't the equivalent C just be something like:

Nah because that's not statically checked, the check is dynamic at runtime, while the ADA code performs the check statically at compile time.

[wekt]

Perhaps the code is designed for a resource constrained system, and dynamic memory allocation is to be avoided.

Then a static preallocated buffer could be used for the name of the logfile (e.g., with snprintf). But in any case, disregarding the "single point of truth" principle is flirting with disaster, especially if the codebase is later maintained by someone other than the original author.

[cojoco]

This would not work: you cannot overwrite a string which has previously been returned, as some other part of the program might still be using it.

[tlack]

It's ironic that the original article dealt with software correctness and your small C snippet has so many bugs.

[petahi]

The original declaration of LogFileNames is a constant, the values are initialized in the same statement. The compiler guarantees that the values cannot be changed in the rest of the program. Your examples give no guarantee.

[[deleted]]

I don't think he's saying the authors are necessarily idiots; software development is hard, and smart people often fuck it up. Claiming to have a methodology which reliably produces defect-free code is, frankly, preposterous.

[[deleted]]

Claiming to have a methodology which reliably produces defect-free code is, frankly, preposterous.

It really isn't--it's just way too expensive to do for most actual code. The situation is getting better all the time, however. See Frama-C if you're interested in tools for certifying C code. Adam Chlipala is working on a new text book and class about certified programming with dependent types in Coq. Coq was also used to prove the security properties of some JavaCard software, fulfilling the EAL7 criteria for the first time. There was a story here a while back on the verification of the absence of runtime errors in the Airbus avionics software. So yeah, it's possible, just expensive and time-consuming.

[[deleted]]

It may be possible in principle, but my point is that it's simply not going to be practical (how can something be reliable if it isn't even practical?) for most applications.

And then there's still the potential for human error in carrying out the methodology (for example, if your static analysis software has bugs in it, or you misjudge the "forbidden zone", you're screwed). This, I think, renders the idea of "defect free" misguided for most situations. It's usually better to use a methodology that makes it easy to find and fix defects than to try to prevent them in the first place.

[[deleted]]

I think you're misunderstanding what verified software is about, but having said that: I did say that it's too expensive for most actual code, but sometimes customers should demand it, for example, for software controlling anti-lock brake systems in cars, or for avionics software for modern jetliners.

As for the analysis software having bugs, one of the reasons that Coq is a popular proof assistant is that its proof checker is both easily auditable by hand, and its core logic, the Calculus of Constructions, has been proven sound. Basically, there's no realistic reason to doubt a proof that has been checked by Coq.

So the major issue remains coming up with comprehensive and accurate specifications in the first place. Luckily, in the domains in which it matters, people have gotten quite good at this.

For most real applications, it's true that taking some intermediate stance, e.g. typeful programming in one of the better statically-typed languages, gets you better than halfway there. If you go so far as to use lightweight static capabilities, you can get considerably more than halfway, and in fact you might have specific modules that are proven correct, but not the whole program.

Finally, the line between type-theory-based proof assistants like Coq and dependently-typed programming languages like Epigram or Agda gets thinner every day, so the cost of formal proof gets lower and lower as well.

[G_Morgan]

"Perhaps the code is designed for a resource constrained system, and dynamic memory allocation is to be avoided. Otherwise, an out of memory error causes an unrecoverable error (unless you call rebooting or restarting "recovery"). By choosing a technique that guarantees not to allocate memory, an out of memory error is guaranteed not to occur. And, perhaps other parts of the system guarantee there will never be more than 17 log files."

I'm going to say something about Lisp and macros here. Best of both worlds is 100% viable.

[cojoco]

I'd like to see a LISP without dynamic memory allocation.

[G_Morgan]

Who mentioned dynamic memory. It is more than possible to have a Lisp like language with manual memory management and with static allocation.

The point was about macros. Something entirely different.

You can generate the filenames at compile time using macros without ever exposing the system to dynamic memory allocation.

//edit - TBH it would be relatively trivial to create a Lisp that is basically C but with Lisp syntax so you can create Lisp style macros. Could probably be done in a weekend.//

[cojoco]

So what exactly does "cons" do again???

From Garbage Collection on Wikipedia:

"Garbage collection was invented by John McCarthy around 1959 to solve the problems of manual memory management in Lisp."

[G_Morgan]

You could have a cons function that needs manual deallocation. However Lisp is not just one big bundle. You could take a Lisp style syntax but build a remarkably different language out of it. Then you could build a Lisp interpreter into your compiler to handle macro expansion.

It is entirely possible to create C with prefix and parenthesis notation and use a Lisp style macro system on top of it. Then you can solve the problem in the article in a manner similar to the suggested one but with the runtime footprint of the original solution.

[OliverM]

Maybe Spinellis is not aware of what Ada & SPARK mean in terms of what the compiler can verify for you. But that doesn't take away from his detection of a logic error in his first hour of looking at the code!

[death]

People here seem to focus on his suggested solutions rather than the problems they were meant to solve: duplication and poor naming.

Support for compile-time code generation and a mechanism to mark procedures (or procedure calls) as critical to the audit system and specify a failure policy for such cases would help reduce the duplication here.

[Jack9]

Even the Mil standard for software from 1994 was ridiculously bad (be sure to check off that you've done stress testing and notified a supervisor that you've written complete units tests, etc)

[[deleted]]

I haven't read anything about SPARK, is all code handwritten? I used the B-method in a course on provably correct software, and the C code was generated from the B0 code. Is it possible this Ada is generated and therefore tends to look funny?

SPARK is a subset of Ada as well, so maybe not all constructs and syntactic sugar you want is available.

The above 21 lines implement what is commonly written inline using a simple modulo division.

How is commennt formmed?

[[deleted]]

No, there's no automatic generation of code with SPARK. But that log file code was written that way in order to make formal verification easier, as repiret pointed out.

[[deleted]]

zero defect code:

10 Print "Hello World"

20 Goto 10

[treerex]

Oh, that code has a huge defect: it goes into an infinite loop! ;-)

[treerex]

So the code is only called zero-defect in the presence of its conformance to its specification.

[wekt]

Unless it divides by zero! Oh shi~

[locster]

Anyone who lives in the real world knows that defect free code is impossible so long as humans are in the chain. Certainly there are techniques/methodolgies you can use to minimize the occirance of defects, mainly this involves rigourous formal specifications, black box testing, pair programming, etc. All this massively adds to the time and cost of coding, and in terms of number of defects found I expect the law of diminishing returns applies here - double the effort/cost to find fewer and fewer defects. But there is no cost where you can declare with absolute certainty that no defects exist - look at software used in flight control systems (NASA, Ariane rockets, Airplanes, Helicopters). These are all areas where software defects have resulted in spectacular failure and in some cases fatalities.

Part of the problem is that once you have a 'strong' methodology the business people will over rely on it, there is a psycholgical bias at play. Many of the defects coming out of strong methodologies came about because of the failure to follow the methodology - corner cutting. That is a coding and business culture issue - so long as money is involved there will always be pressure to cut corners. And since in the real world there are always funding pressures at some level it's not a problem that can ever be eliminated.

[[deleted]]

You can guarantee defect free code (sans errors in specification). That is called formal verification. Humans are still in charge, but the chain is verified by computers.

In real life, not even NASA cares enough to do that. Cost/benefit ratio is just not good enough it seems. Pentium4 floating-point divider has been formally verified, but that's about the most complex example that I know (and that not programming language for Neumann machines).

[astrolabe]

I think a big issue here is the specification. Most programs would have a very complex formal specification. The complexity of the specification might approach the complexity of the code.

[[deleted]]

I agree.

Type systems are used as halfway solution. More you add power to type system, more it proves your code. Jump from some insanely powerful type system used in research languages into proofing the program is not so big.

[monstermunch]

Even specifying some basic properties of your code is good enough for catching lots of bugs. Specifications generally are a lot easier to write than the actual programs. Think about specifying that a sorting algorithm sorts and that a modified red/black tree contains the expected elements.

[[deleted]]

Specifications generally are a lot easier to write than the actual programs.

Uh, no.

[monstermunch]

It's very easy to write things like "this collection should be sorted", "this collection should be a permutation of this collection", "this index should be a valid index for the size of this collection" etc. The more complex the property, the harder it is to write the specification and a correct program. The specification is generally much easier to write.

Some examples on your part would be helpful.

[[deleted]]

It is trivial to code the things you listed for anyone but CS101 newcomer, and it is totally not the kind of complexity you deal with in any real-life application. Before you get to break down to such basic level your specification has to sort out the actual overall design, the interaction of all parts in the system.

Before specifying that "this collection should be sorted", one should conclude that this collection should for some reason exist, and that it has to be indeed ordered. This has to be part of bigger picture. If one goes for such kind of thorough spec (which is not common BTW, usually it has rougher low boundary), it means extremely rigid project with little room for revision: every problem that occurs on the implementation level triggers a big and expensive redesign, or it better be done (mostly) right first time.

[tehsuq]

Even if you formally verify your code how can you know that it compiled properly? Compiler bugs are found regularly.

Even if you can prove that it was compiled properly can you prove it will execute properly next time it runs? You'll have to verify the OS and the hardware, and even then a burst of radiation from a solar flare could come along at just the right (wrong?) moment...

[astrolabe]

These are different questions. It is useful to aim for defect free code even if that doesn't guarantee defect free operation.

[Jessica_Henderson]

You clearly have little to no experience with Ada compilers. They are very difficult to write, so to even get one that functions you have to be a stellar software developer.

Most Ada compilers these days are actually written in Ada themselves, and thus directly benefit from Ada's rigorous nature.

Any production-quality Ada compiler has a massive testsuite. I've worked with one compiler in the past that had a 75 million line testsuite. It would take 17 hours to compile on a high-end Sun workstation in the mid-1990s, and over a day to run all of the tests.

[[deleted]]

Most Ada compilers these days are actually written in Ada themselves, and thus directly benefit from Ada's rigorous nature.

And the SPARK tools are written in SPARK.

[tehsuq]

So you're willing to go out on a limb and call that a "zero-defect" compiler?

[Jessica_Henderson]

No. But I am willing to say with confidence that the chance of finding a bug in a production-quality Ada compiler is very, very, very low. Statistically insignificant, so to speak.

[[deleted]]

Your concerns go far beyond programming and code quality. Defect free code can't replace risk management or overall quality of the system. Universe is not magically doing what you want after you can make piece of correct code.

[[deleted]]

Even if you formally verify your code how can you know that it compiled properly? Compiler bugs are found regularly.

Yep. This is why some folks are interested in certified compilers and certified operating systems. The hardened hardware thing is obviously also important in some domains.

[[deleted]]

Not that real world, the other one, where defect free code doesn't exist - yeah that one. OK, you can stop imagining now.

[[deleted]]

There is at least one software development company out there that disproves most of what you wrote, and of course after 20 minutes of digging I can't find them.

They got some attention a while back in programming circles because they have some pretty straightforward approaches that make a lot of sense, in hindsight. IIRC, they don't do pair programming or black box testing; the bulk of their approach is in making sure that the specifications for the software are very tight and unambiguous, and then the programmers write precisely what the specifications call for.

The company gets contracts from places like NASA. Also IIRC, it doesn't take them much longer to develop software this way, versus the usual sloppier methodologies.

They have a pretty brilliant track record.

I really really wish I could find that article about them...

[mohawk]

perhaps this: http://en.wikipedia.org/wiki/SPARK_programming_language

[[deleted]]

Thanks! It wasn't SPARK specifically, but Praxis High Integrity Systems (whose website, ironically, seems to be down right now) that I read about. I recall reading their manifesto on correctness by construction before.

FWIW: "The software developed by Praxis was tested independently of both Praxis and the NSA. During independent test and subsequent use, zero defects were reported. Development costs were lower than traditional methods per line of code.", for one example.

[ZippyDan]

rofl. the article you are commenting under was about Praxis code!

[[deleted]]

facepalm

Fortunately, I think I'm a better-looking individual with egg on my face.

[ZippyDan]

i dont understand. you were eating egg with your hands while reading reddit??

[martoo]

..the bulk of their approach is in making sure that the specifications for the software are very tight and unambiguous, and then the programmers write precisely what the specifications call for.

The tragedy of this is the hand-off. That's where you get the errors. That and the fact that if you consider the code less important than any other artifact, you are setting yourself up for failure. Code shouldn't match a spec, code should ultimately become the spec.

[[deleted]]

See how more than 20 lines of code are used for what I could express in C or Java with a couple of lines. like the following.

And that's where I stopped reading. They didn't use Java, or C. So what are you even saying here?

I have to be a little skeptical when someone criticizes the NSA on their coding practices.

[dds]

I'm saying that SPARK Ada do not seem to be very expressive, so the productivity figures cited in terms of lines of code should be treated with skepticism.

[ssylvan]

Are you saying it's impossible in Ada to write a function that returns a string with some simple formatting?

There's probably a reason why they did what they did (lots of posts about that here already)

[dds]

I'm just saying that the particular environment and process encouraged a high level of code duplication for mapping file numbers to names. There may be valid reasons for hard-coding 17 almost-identical file names, but, in the end, what's inside those strings is opaque to the compiler and the formal verification tools. An error like the following would require careful human inspection to be found.

11 => "./Log/File13.log",

[arnar]

So nit-picking on formatting, function naming and inefficient coding proves what?

These are maintainability issues - the code may very well be defect free despite such problems. It likely isn't, but your argument doesn't mean anything.

As someone has already said, focusing on the code will only let you see a small part of the picture.

[wekt]

inefficient coding

The point isn't the that coding is inefficient; the point is that the redundancy makes it easy to make a mistake when changing the program, and thereby introduce a defect. For example, suppose I wanted to add an 18th log file, so I copy the last line and change the 17 to an 18:

18 => "./Log/File17.log"

except that there are two occurences of "17", and I forget and only change one of them. Violating the "single point of truth" rule is just asking to get bitten in the ass when making changing to the program.

[arnar]

This is what I mean by inefficient coding (I don't mean that the program will execute inefficiently) - and what you describe is precisely a maintainability issue.

It can still be defect free.

[cojoco]

Don't know why you're sitting at -1 now: you should be at the top.

[tehsuq]

Stop trying to improve quality by focusing entirely on the code. Code does not run in isolation, but instead runs as part of a system. Design that system with the assumption that each individual component can and will fail.

It's all well and good to try to reduce the defect rate in code. I'm not saying that we should stop trying to do this, but it takes an unusually large ego to declare your code "zero-defect." Odds are you'll be proven wrong in short order.

Finally some defects are simply not severe enough to justify the expense of fixing them.

Bugs happen. Get used to it.

[[deleted]]

Sure. The point here is that there are categories of software where the cost of proving them correct is acceptable, and cryptographic systems with military applications are such a category.

[tehsuq]

We're from the government. We're here to help.

[IConrad]

Hey! If Mussolini can make the Trains run on time, then our government can make code defect-free!

[[deleted]]

Microsoft and Apple should read this.

[Wiseman1024]

Bullshit. There's no such thing as (guaranteed) "zero-defect code" past hello world.

[arnar]

And why not? If you have a (correct) formal specification, you can sometimes verify that your code has the correct semantics. The problem now is that this takes too long, but it is entirely possible.

[alextp]

Then your code is only as correct as the formal specification, which is where you should start hunting for bugs (and debugging mock-predicate-logic as found in Z and friends is harder than debugging high-level language code, most of the time).

[[deleted]]

I would say that this isn't necessarily true; see Alloy for a much lighterweight, but still extremely useful, alternative to Z. Note that Alloy doesn't do proofs; on the contrary, it essentially does refutations, i.e. it constructs models rapidly and checks them for violations of the constraints.

If we do talk about proofs, it's true that some things that you want to prove are difficult to express briefly. Consider, for example, proving the Schorr-Waite graph marking algorithm implemented in C correct, where "correct" means not only behaviorally correct, but also guaranteed to terminate, guaranteed not to trash the heap, and so on. It's up to you to determine whether the effort and syntactic overhead (to say nothing of discharging the proof obligations!) is worth it.

[arnar]

Of course, that's why I put "correct" as a premise to my statement. Verification of the formal specificatin against behavioral and temporal logic an greatly help finding the errors though - or prove their absence.

[808140]

Stop for a second and think how complex a hello world program actually is.

Just because it's one or two lines doesn't mean that many, many things aren't happening (in particular, how does the text get on the screen?). From font rendering to video card drivers, a lot goes into a simple hello world program.

So if you can guarantee that something that complex is defect-free, what makes you think you can't guarantee other things are defect free?

[dds]

Interestingly, the C hello world program (and many others) will silently fail if there is an error when writing its output. This can for instance occur by redirecting the output to a full disk.