Is Code Verification Finally Good Enough?

Jonathan asks: "As someone who has been following the development of software verification technology, a recent trend has intrigued me. It seems that the formal method people have finally come down off their high horse and are offering code verification as just another tool. This approach shows up in recent Java and C# based code verification tools that aren't aimed at 'proving correctness' so much as finding potential errors. Now it seems that such an approach is beginning to find its way into XP methods[pdf] as another verification tool to supplement unit tests. Given the current speed and effectiveness of tools like the Spec# verifier, is code verification via automated theorem proving finally going to make its way into the mainstream?"

For what?

[Control Group]

What does "good enough" mean? Good enough for it to be included as a general-use software development tool?Good enough to guarantee that released code is bug-free? Good enough to guarantee that released code has no glaring security-affecting errors?

It makes a difference which "good enough" you're asking for.

(The answers to those questions, to channel one Urban Chronotis, are yes, no, and maybe. Not necessarily in that order)

Re:

[Peter La Casse]

In my experience, the "good enough" that matters is "good enough to catch errors without forcing a developer to have to think." When it's click and drool, and yet still useful, it will be "good enough" for widespread adoption.

What should be verified

[derek_farn]

Before tools [wikipedia.org] can check the code (eg, static analysis [wikipedia.org]) we need to know what constructs they need to flag. The formal verification people will claim that checking a program's source against its specification is the solution. However, that is a very expensive and time consuming process. There is an ISO group looking at vulnerabilities in programming languages [aitcnet.org].

For Guaranteeing Correct Requirements?

[billstewart]

• Do theorem provers prove that what the user told you they wanted made sense?
• ... that what they wanted would solve the problem they were trying to solve?
• ... that the problem they thought they were trying to solve was really the problem they *needed* to have solved?
• ... that what they wanted when you started was still what they wanted when you were done?

Uh... no.

But they can probably be considered to be a newer and better version of lint, and that's a good thing.

Re:

[tom's a-cold]

Mod parent way up.

Code-checking is a good thing, and provably correct code is especially good, though what's provable is still narrower than the range of behaviors of any interesting system I've seen.

But the most difficult part of any complex system development project is getting valid requirements and then implementing a process of systematically and iteratively confirming that the delivered system is what the users need, not what some bunch of managers or analysts asked for on their behalf. This is

Slowly work their way into the mainstream

[pdovy]

I think it's legitimate to expect verification tools to make their way into mainstream software development, but not as any sort of "catch all".

Developers will have to analyze the specific tools and decide if it is a good supplement to current verification efforts or if it can replace some steps. I think though once it worms its way into mainstream (if only light) use, the tools will continue to improve and give us more options, and become a more integral part of verification.

I know from work I've done, th

"No"

[quiberon2]

Mankind's ability to write software is far in advance of mankind's ability to figure out what it does or does not do.

If Microsoft ship 100 million copies of Windows Vista to 100 million people on public Internet, where the people have mutually-incompatible agendas, then at least some of the people will end up unhappy.

a chain of crutches

[fred fleenblat]

I dunno, as more tools to verify code become available, businesses will hire cheaper and sloppier programmers and just force all the code through the verifiers and hope for the best.

These aren't tools to make the best code better, they are tools to make the worst code okay.

Re:a chain of crutches

[chroot_james]

they already do! I came across this the other day:

private getThis() { return this; }

Re:

[kirun]

Seems like sensible future-proofing to me. Sure, the variable this is called this right now, but who knows what tomorrow will bring?

Re:

[dgatwood]

It got funnier the more times I read it. The first time, I read it as a private accessor function that returned a private class member. That alone would be funny, since the only reason to make such a function would be to allow read-only exposure of a private member to non-class code, and by making it private, that eliminated the usefulness altogether. Then, I realized precisely which member was being returned. When I realized that it wasn't returning an explicit class member, but rather, a pointer to th

Re:

[lokedhs]

The method could be overridden in a subclass. That would make it useful.

Or perhaps the .getThis() method was specificed by an interface as a way of retrieving some functionality, but the functionality was implemented by the class itself. This design is used in table cell renderers in Java for example.

Re:

[DragonWriter]

Tell me that's a joke, and no one actually wrote that in a serious program.

Or at least, if they did, its in a language that just happens to look like Java, but where "this" isn't a reference to the object the object the private method is in. Because that makes my brain hurt.

Re:

[MightyYar]

I've never seen anything quite that bad, but I do see this a lot in older code:

private getThis() { return get_value(foo,bar); }

The explanation for that is often that someone will create a function to go fetch a single piece of data, getHeight(). Then the next programmer comes along, and adds the ability to getWidth(). The next guy starts to add getDepth(), but then thinks that this is a bad path to go down, so writes a new function called get_value() that serves the more general purpose of fetching data

Re:

[mindriot]

This brings up a somewhat interesting point. I can see the point of using stuff like getFoo() just to access an attribute foo. I think it has its purpose (read-only access), but I can also see that it is rather ugly. Further, in C++ code you sometimes see the use of friend just to provide full access to certain attributes and methods otherwise kept hidden or read-only (through getFoo()) to certain privileged classes and such.

I think sometimes it might be more useful to provide proper access control f

Re:

[aminorex]

that wouldn't compile anyhow, so it's not surprising that we don't know what it is for.

Re:a chain of crutches

[neutralstone]

Regardless of the poor decisions of some recruiters, I've found this to be true: the most competent and disciplined engineers tend to use as many checking techniques as possible (e.g., regression tests, unit tests, multiple static analysis tools, etc.). They use these techniques not as a substitute for a disciplined approach to design or to implementation (that would be foolish), but as a sanity check on a finished product. They use multiple checking techniques because they know they're human, and humans -- even the most skilled, most experienced, most disciplined ones -- make mistakes, and they want to do everything they reasonably can to catch mistakes before a product ships.

So to that end, model checkers (and other forms of checking) are Good Things(TM). The possibility that some will misconstrue checking facilities as a substitute for competent and disciplined engineers is a separate issue, and it's not the fault of the checking scheme. The *organizational* problem of poor recruiting cannot be solved by getting rid of model-checking systems, and if your recruiters think that talent can be replaced by a "verification" system, you've got bigger problems than merely the shoddy designs that will come down the pike.

(Please note that I prefer to use the term "check" rather than "verify", because the latter term, when used to describe a program, too easily connotes the notion that a "verified" program is free of any bugs (which is, needless to say, always a dubious claim). "Check" on the other had usually connotes the idea that there is a specific bug (or set of specific bugs) that is tested for. Of course, TFA mentions they don't want to imply that (verification == no bugs). But IMHO too many people make that mistake.)

Re:

[palantir0]

I've found the complete opposite to be true. Rarely do I find tons of checking tools. Mostly it is design review the arch, implementation, and code. Perform unit testing. The good engineers do better unit testing, thinking about the interactions, wake up at night realizing something is screwed up, and fix their problems proactively.

Everyone 'wants' to use tools but the reality is the overhead is pretty significant so they are avoided. Only in large companies do I see this methodology and even that is f

No

[Gemini_25_RB]

Finding errors /= Proving correctness. Part of proving a program, imho, should include making sure the program only does what it claims to do. No more. (Say goodbye to tag-a-long malware!) Of course, this is a pretty idealistic outlook. We could all just program in ML, instead.

Not possible

[Intron]

The problem with any verification tool is that it can't know what you expect the program to do unless you tell it. Why should this be any more correct than the program itself? In other words, if you can write a description of what the program should do that is more accurate than the program, then that description should replace the source code.

Re:

[Intron]

Your example 1 - if the verifier checks to make sure the passed argument is an l-value, then the compiler should be able to make the same check, which is what I said.

Your example 2 - of course it's easy to check if the result is sorted. That's called QA, not verification. Verification would be proving that the quicksort routine sorts the array for all possible inputs. Proving that it implements quicksort and not a sort that has slightly worse performance is an even harder problem.

So no, you did not dispr

Re:

[Eivind Eklund]

For some reason, you took this in the spirit of "something you should argue against" instead of something you should learn. Now, I'm perfectly willing to argue and show that you've been behaving as an ass, if that's what it takes for you to LEARN, NOW. So, to make you LEARN NOW, I'll do the shouting and behaving in your spirit, increasing the magnitude a bit so you can GET IT.

You see, you totally missed the point of my comment. (A) "The compiler could do it" is the same as saying the compiler is a veri

Re:

[tricorn]

There are many simple things that a program verifier can check for. I can see a program figuring out that your foo(NULL) call is always going to be wrong (e.g. by having the verifier notice that you are dereferencing it without checking if it is NULL and adding an assertion to the exported definition of the function; in this case the assertion will be a constant so it can be a compile-time error).

A lot of the "variable may be uninitialized" errors that a good compiler will spit out are along those lines.

Re:

[MarkusQ]

However, even gcc complains about c being possibly uninitialized, even though we can tell from looking at the code that n MUST be greater than 0, so on the first pass through the code, the second if clause must be true, thus c will always have a valid value.

This is a good example of why code verification is a hard problem. You may be able to tell from the given code fragment that c is always initialized, but I can't. Specifically, when "float n = 0.5;" it seems to me pretty clear that c isn't initiali

Re:

[tricorn]

You make a good point, but since I was only giving code fragments, you didn't see that this was C code and n was declared as an int parameter...but, let's say it's a dynamically-typed language, should it flag this code fragment as the error, or the location where I call it with a value that it can't prove is = 1? You can go a long way with assertions, and a program verifier can use assertions to guide it in it's proofs (although the assertions have to verifiable from the code, which means you have to lay o

Re:

[dctoastman]

What if n is less than 0? You say that by looking at the code that n must be greater than 0, but that is nowhere in there. There is no check on the value of n so you can't assume the value.
Then c and b will both be uninitialized.

You can't trust initialization in conditional statements unless you cover all conditions or if you declare your variables within the conditional code block.

Re:

[tricorn]

b and c will be uninitialized outside the loop, true, but they aren't used outside the loop. Note that I don't declare the variables, inside or outside the loop, and it isn't even necessarily C code. Even if b or c are used later, it could well be that they are used in a context where n is known to be >= 1. You can't read more into code fragments than what is presented.

If I were to use b or c after the end of the loop (with no other initializations or conditions), then a program verifier might add in

Re:

[dctoastman]

So your only defense is that it is a fragment. By that logic, since it is a fragment, you can't assume that b and c won't be used after the loop either. You are reading outside the code fragment if you assume they won't be used. And if you want us to assume anything about the code that isn't explicit, make it explicit. If your code fragment was instead wrapped around this:

void function(int n)
{
//Your fragment
}

Then your arguement would hold water, but as it is hope for the best, but plan for the wors

Re:

[tricorn]

I don't need a defense, I was giving an example of code that current compilers don't analyze as completely as possible, as an example of the type of thing that a code verifier would have to be able to analyze in order to find obscure problems. It wasn't being held up as an example of fine programming.

I don't need to assume anything about b and c outside the loop, as I didn't give any code outside the loop. You're the one assuming for some reason that b and/or c would be needed after the loop. I was sayi

Re:

[Anonymous Coward]

Exactly right. How can a program know what another program is *supposed* to do unless the first program has available to it an exact description of what the program it is checking is supposed to do? And if that exact description is available, there should be an automatic code generator which turns the description into code.

In other words, writting the exact description of what you want should be your last step in development, after which a code generator creates the program. This turns coding into the pr

Re:

[l33td00d42]

Alice: "Try to get this concept through your thick skull: the software can do whatever I design it to do"
(pause)
user: "Can you design it to tell you my requirements?"

boy, that's easy:

print "This software is required to print this statement.";

Re:Not possible

[rblum]

That - in an other discipline - is called "double bookkeeping". You specify things twice, independently. Once in the actual source code, once in the description.

That way, you'll know when the two disagree. It doesn't prove that it does what you *intend* to do, but it proves that spec and source say the same thing. If they're written by different people, you can now have a fairly high degree of confidence.

Does it make your program bug-free? Only if you can write a bug-free spec. But it's a useful concept to reduce the likelihood of problems.

Use a language with build in prooving.

[krischik]

There some programming lanugages (Ada, SPARK and Eiffel spring to my mind) which have the verification build in (to some degree). Just in case you wonder how that works here my favorite Ada example:

type Day_Of_Month is range 1 .. 31;

Neither Java nor C# allow that kind of controll over integer types. Mind you there is A# (Ada for CLI).

Martin

Re:

[bodan]

There some programming lanugages (Ada, SPARK and Eiffel spring to my mind) which have the verification build in (to some degree). Just in case you wonder how that works here my favorite Ada example: type Day_Of_Month is range 1 .. 31; Neither Java nor C# allow that kind of controll over integer types. Mind you there is A# (Ada for CLI).

Well, they don't quite allow this control on integer types. But you don't need to use integer types, you can use an enum in Java (with methods for operations), and I _th

Re:

[krischik]

Well, you are right - you need a Date class. It is all about refined. As long as you don't know the month you can't check the date further the 1..31. It's kind of a first step.

Once you know the month inside a Date class you can do more checks. But you won't need to check for the date to be >0 or 32 any more - theese cases have allready been handled.

Martin

Re:Not possible

[Coryoth]

The problem with any verification tool is that it can't know what you expect the program to do unless you tell it. Why should this be any more correct than the program itself? In other words, if you can write a description of what the program should do that is more accurate than the program, then that description should replace the source code.

It is often easier to describe what a program has to do than it is to describe exactly how to do it. I can describe what a square root finding algorithm has to do: given x it has to find y such that y*y =x; without coming close to writing something that actaully finds the square root. All the prover then has to do is ensure that the code instructions really do produce a result that satisfies the stated constraint - which is potentially entirely possible. Writing contracts for code can be as easy (or easier) than writing unit tests for code. If you write a contract instead of a unit test then that potentially gives the prover all it needs to verify that the code will work for all possible test cases instead of your predefined unit test cases. If the prover can't manage that then just feed in some test data and if the contract fails you've found an error (that is, at worst you've got a unit test already). Working this way can be remarkably efficient at weeding out errors - you verify code when it works, and essentially do unit testing for the code that can't be verified. Perhaps if you actually tried it you'd see.

Re:

[FrostedChaos]

A very informative comment. I especially like your description of type systems as theorem provers.

I agree that it would be nice to see some simpler, cleaner languages, but I'm not sure if that's going to happen any time soon. For example... suppose the people who design model checkers for SML only have to do only X man-years of work, while the people who do model checkers for C# have to do 100X. So what-- the model checkers for C# are still going to be cheap and widely available, because there is a market f

Re:

[Peaker]

The problem with any verification tool is that it can't know what you expect the program to do unless you tell it. Why should this be any more correct than the program itself?

Many aspects of the program can be described, and not all of them must be proven.

A program can be roughly divided to its requirements specification and the implementation. The requirements leave a lot of "freedom" to the implementation, and the choices in this area are not important to prove.

As a simple example, a "sort" algorithm has

Excuse me, did any of you graduate yet?

[Anonymous Coward]

Since when did this move from the realm of undecidable problems into solvable with a Turing Machine?

Re:Excuse me, did any of you graduate yet?

[Fahrenheit 450]

Well, it's quite possible to do things like restrict the problem to a decidable subset of the original problem and only let your solution work on those subsets. Or you can work on problems that are undecidable in general, but in most typical cases are not only decidable, but efficiently solvable. For example, most type systems work in one of these two ways.

You see, you should have learned before you graduated that just because a problem is hard (or impossible) in general, that doesn't mean the average case is hard at all.

Re:

[UncleFluffy]

Since when did this move from the realm of undecidable problems into solvable with a Turing Machine?

About as long as we've being using finite state machines as approximations to a Turing Machine.

No :)

[Monkelectric]

The thing you have to remember about methodologies is they are all bullshit. In my experience, the people who cling to methodologies are generally not clue-full.

The paper you linked to -- I just finished reading it. The "methodology" they provide has more comedic value than anything else. The steps in his methodology are counter-intuitive and therefore stupid. He wants us to iterate over each requirement, re-writing a function as the most simple program which passes the tests? What possible reason fo

Re:

[Monkelectric]

The problem he's solving is not one of "How do I write this?" but "How do I write this, be able to change it, and know that it still works the same?"

I *REALLY* think you miss-interpreted the problem. The author clearly states the task is to build a function which gives all prime numbers smaller than n. Furthermore, what you've described is unit testing, which sadly is not a new concept.

Re:

[Peter La Casse]

The thing you have to remember about methodologies is they are all bullshit.

Not every methodology sucks all the time. A methodology is just a named collection of practices.

In my experience, the people who cling to methodologies are generally not clue-full.

Humans inherently crave religion. Convince someone that something works and they're likely to cling to it to the bitter end, be it Code Verification, atheism, voting Republican or whatever.

Re:No :)

[Control Group]

The steps in his methodology are counter-intuitive and therefore stupid

I agree with your general statement, but this isn't good evidence. Plenty of things are counterintuitive, yet correct and useful.

I present exhibit A: the whole of statistics. It is counterintuitive that after the tenth straight "heads" result, the eleventh flip still has even odds of coming up heads - despite the fact that the odds of eleven straight flips coming up heads are 2048:1. It is counterintuitive that you should always switch doors in the Monty Hall problem.

Or, if you're scientifically minded, I give you relativity. It is counterintuitive that no matter how fast you're moving relative to a light source, the speed of the light from your point of view will never change.

It is counterintuitive that gravity causes hot air balloons to rise, or that the way to escape Earth orbit is to accelerate along it, not away from Earth.

Counterintuitive doesn't necessarily mean that something's incorrect.

Re:

[tricorn]

"The way to write software is to design it, not have a random number generator spit out text, wait until a given chunk compiles, then test it to see if it does what you want."

And you say "that's not true, it will eventually produce a correct program! It might be easier to write a program by designing it, but that's a different question."

Anyway, if you are in orbit and you continually accelerate directly away from Earth (which means that you are continually changing your thrust vector as you continue to or

Re:

[aminorex]

"The way to write software" smell like a method to me. Methodology is simply the study of method, or more broadly, any discourse on the topic. A statement beginning as quoted is a methodological claim.

A lot of good code has been written using genetic programming and genetic algorithms, so I find it to be an erroneous or at least over-broad claim.

Re:

[Profound]

>> It is counterintuitive that gravity causes hot air balloons to rise

That's buoyancy.

Yes, it works, but it's not easy

[Animats]

The main reason program verification didn't catch on was that it was hopeless for C and C++. The semantics of those languages were so messy that formalizing them was nearly hopeless.

Java and C#, however, are good enough. (So were Pascal, Modula, and Ada.)

Here's the manual for the Pascal-F verifier [animats.com], a system written by a team I headed back in the early 1980s. This was a proprietary system done internally for Ford Motor Company. Take a look at the example real time engine control program beginning on page 155. It was painfully slow back then; it took 45 minutes of VAX 11/780 time (1 MIPS) to verify that program from a cold start. Today, it would take about a second.

What's being proved in that example? First, that there are no subscripts out of range or arithmetic overflows. Second, that all loops terminate. (Yes, you can prove that for most useful programs; the halting problem applies only to pathological programs.) Third, that the following constraints hold:

• fuelpumpon implies (tickssincespark < (1000*ms)); if fuel pump is on, spark must occur within 1 sec.
• (enginespeed < rpm(1)) implies (not fuelpumpon); fuel pump must be disabled if the engine is not rotating
• cylssincespark <= 1; a spark must be issued for each cylinder pulse

Useful stuff, the conditions needed to keep the engine running.

This is "design by contract" with teeth. Each function is checked to insure that it always satisfies its exit conditions if its entry conditions are satisfied by the caller, and that the function doesn't overflow, subscript out of range, or fail to terminate. Each call is checked to insure that its entry conditions are always satisfied. The end result is a guarantee that those properties hold for the whole program.

This is a very valuable check. It insures that caller and callee are in agreement on how to call each function. That's the cause of a huge number of software bugs - the caller made some incorrect assumption about the function being called, or the function didn't check for something which it needed to check. Both of those can be statically machine checked.

It's not easy to get a program through formal verification with a verifier like that one. The verifier does almost all the work on easy sections of code, but where correctness depends on anything non-trivial, you have to work with the theorem prover to get the proofs through. This isn't easy. The DEC Java checker and Microsoft's Spec# checker aren't as hard-line.

Re: (So were Pascal, Modula, and Ada.)

[krischik]

Well at least Ada still is: http://www.praxis-his.com/sparkada [praxis-his.com] and very successfull as well.

And Ada isn't dead, it just got another rejuvenation in the form of Ada 2005: http://www.adaic.com/standards/ada05.html [adaic.com].

So the use of past tense was not appropiate.

Martin

Re:

[hritcu]

Who is using Ada? [gwu.edu]

Re:

[krischik]

http://www.adacore.com/home/ada_answers/lookwho [adacore.com]

I work for one of the named companies ;-) and for our "mission critical" applications we have no intention to change.

Re:

[Peaker]

The main reason program verification didn't catch on was that it was hopeless for C and C++.

Java and C#, however, are good enough. (So were Pascal, Modula, and Ada.)

What is the semantic difference between C and Pascal?

As far as I can remember, the only real semantic difference was Pascal's lack of casting.
Is this difference really the breaking point of C's provability?

I would expect pointer arithmetic to be the source of problems, but if I recall correctly, Pascal's pointers have arithmetic as well.

Re:Yes, it works, but it's not easy

[Animats]

What is the semantic difference between C and Pascal?

The big problems with C/C++ from a formal methods standpoint:

• void* (You lose all the type information)
• Too much casting. (Again, you lose all the type information)
• Array size information isn't carried along with arrays or passed through function calls. (Biggest design mistake in C).
• The "array is a pointer to the first element" convention. (Is this an array or a single object?)
• Pointer arithmetic semantics are ill defined. (Long story.)
• C++ iterators don't have an explicit tie to the collection, so detecting iterator invalidation statically is hard.
• Hard to detect aliasing. (A consequence of the free use of pointers.)
• Too much "undefined behavior" that isn't prohibited.

I would expect pointer arithmetic to be the source of problems, but if I recall correctly, Pascal's pointers have arithmetic as well.

No, they don't.

Pointer arithmetic really is obsolete. Compilers have been generating code for subscripting that's as good or better than pointer arithmetic code for well over a decade now.

Re:

[StrawberryFrog]

I would expect pointer arithmetic to be the source of problems, but if I recall correctly, Pascal's pointers have arithmetic as well.

No, they don't.

That depends entirely on what you mean by "pascal". The pascal language as spec'd doesn't. But nobody uses that, so this not a very useful definition to adhere to.

Most users of "pascal" use/used Borland Turbo Pascal or Delphi. In those languages you *can* do pointer arithmetic. Sure you have to jump through more hoops and casts than with C (it can be considered

Re:

[krischik]

Others answered the question but I can add practical experience here. For A while I tied splint [1] and after after a while it became clear that the greatest problem whas the lack of array bound.

I tried hard, realy hard to get splints bound checking to work - but in the end it did not work out.

The project is not stalled since 2004 [2] and for me it is now clear that the "Secure Programming Lint" was a hopeless endeavor.

As for casting: Ada has about 3 different ways of type convertions and is still provable.

Re:

[Peaker]

PS: I have programmed in Ada, C, C++, Java and Pascal and my favorite language is now Ada.

I have programmed in Assembly, Python, C, C++, Pascal, some Lisp and a tiny bit of Java, Haskell and Ada.

I dislike Ada because I believe there are far too many primitives that should be libraries (semaphores and other concurrency features).

I now love the other edge of the spectrum: Python. The "eww whitespace" barrier seems to block/filter a lot of closed-minded programmers, but don't let it prevent you from learning

Semaphores in Ada

[krischik]

But Ada does not expose the use of Semaphores - The task model of Ada is based around Rendezvous.

There are some attempts of Rendezvous based threading for other languages but it proves difficult since you need some inter-task parameter passing mechanism. Remember that a Rendezvous is a bit like a function/procedure call only the parameters are passed from one task to another.

And parameter passing is a language feature and quite difficult to implement as a library. I know because I tried using by using Obser

To quote Knuth

[dargaud]

"Beware of bugs in the above code; I have only proved it correct, not tried it." —Donald E. Knuth.

logic bug

[hey]

How could a program ever find this bug:

if (vote == "democrat")
{
        republican++;
}

Re:

[vidnet]

Simple, it would see that "democrat" was a literal and thus it would be highly unlikely that 'vote' would happen to have that same pointer value, and it would suggest if(strcmp(vote,"democrat")==0) instead.

(haha)

Re:

[Brown]

It's not a bug, it's a feature!

Verification gets a boost from managed langs

[icepick72]

Verification is speeding along because of managed languages. Verification for managed languages like Java and C# is easier to implement. Not so much for C/C++ where pointers are raw. (Note: C# allows unmanaged code but by default it's managed and I assume most developers work in C# in managed mode, except where performance or interopability is required)

Please verify:

[RAMMS+EIN]

``Is Code Verification Finally Good Enough?''

Please verify that

(define (foo n)
        (cond
                ((= n 1) 1)
                ((even? n) (foo (/ n 2)))
                (else (foo (+ (* n 3) 1)))))

returns 1 for any positive integer n.

Well typed-ness matters, not the halting problem.

[DamnStupidElf]

Anyone can come up with a list of algorithms for which the answer to all inputs is unknown, of which the 3n+1 problem is one (so far). Even though we can't prove that the algorithm halts we can still prove that it's well typed, which in practical terms is much more important because it prevents buffer overflows and any number of other programming errors. In addition, we can also prove that the algorithm actually does solve the 3n+1 problem and not some similar but slightly different one. For instance, if yo

Re:

[RAMMS+EIN]

``Even though we can't prove that the algorithm halts we can still prove that it's well typed, which in practical terms is much more important because it prevents buffer overflows and any number of other programming errors.''

For preventing buffer overflows, you will have to prove that some value being used as an array index is an integer in the range from 0 to the size of the buffer minus 1. In this case, the problem is to prove that the result is an integer in the range 1 to 1. Most type systems aren't exp

Re:

[DamnStupidElf]

For preventing buffer overflows, you will have to prove that some value being used as an array index is an integer in the range from 0 to the size of the buffer minus 1. In this case, the problem is to prove that the result is an integer in the range 1 to 1.

Generally, proofs for this are expressed as loop invariants inside of functions, and as predicates on the entry and exits of functions. If a function takes an array index as a parameter, there is a predicate that 0<=i<n, and it is the responsibi

Re:

[FrostedChaos]

Ok, I have a program that, if it halts, causes a buffer overflow.
Otherwise, it doesn't.

Can your type system prove that there is no buffer overflow?

Coming from the hardware side...

[netchipguy]

Formal Verification has become a staple of hardware design. It basically comes in two forms: equivalence checking (used a LOT to compare two similar designs) and model checking (which is slowly making inroads; used to compare a design against a set of rules, another model, etc).

I have often wondered why more formal techniques aren't deployed in the software world.

As has been mentioned here, the thing about formal is that you will often "stump it" and so you may need to "help it" in complex, real world desi

Re:why more formal techniques aren't deployed

[lwriemen]

Because too many software "craftsmen" think "methodologies ... are all bullshit". They believe they are artists, not scientists, and reject rigor as untried academic exercises that stifle creativity.