> What seems complicated?> > For example here:> http://rifers.org/09_stateful_counters/src/> There's no XML file in sight.> > > Some people like external XML declarations, some don't.> You use what you need. Like for example this:> http://rifers.org/08_advanced_continuations/src/> > What does a checkout process. The XML hardly seems complex> to...

> From this the compiler should be able to use the same> reasoning as is needed for fact(). Of course, if fn loops> forever, map will never return either...> > > ; counts the leaves of a tree > ; count-leaves('(2 3 (5 5) 4)) => 5 > > count-leaves(x:pair) = count-leaves(car(x)) + > count-leaves(cdr(x)) > count-leaves(nil) = 0 >...

The approach seems extremely complicated. Why should a developer go through all those hoops and not use something like Echo2 (simple Java-only programming without XML and other funky stuff) ?

Wouldn't top-to-bottom construction be more useful in the case of 'boiling ocean'?

> I think it's possible to prove it. If you can prove that> the recursion will always hit the base case you're done.> You can prove that n will get closer to the base case.> That's pretty easy to prove. But if you evaluate fact(4.5)> it won't stop. You don't have this problem in this case> because the function only accepts integers, but there>...

> > line 9 : n1 is a legal value for passing it to 'fact',> > because n1 >= 0. Since n1 is a subset of n, the end> result> > is 1 (already computed), so f can only be a positive> > number.> > Do you have any ideas about the implementation of this,> specifically this: > > "the end result is 1 (already computed), so f can only be> a positive...

> This sounds interesting. Do you have any ideas about> recursion?> > For example:> > f = a b [f] if> > How do you make sure that the output of f is correct if it> depends on f itself (and maybe on the correctness of f)?Let's see the factorial function (written analytically). The contract is that the input is greater than 0:1 int fact(int n : n...

> I did reply on March 21st:> > Hi Achilleas,> > I'm sorry it took me so long to get back to you. This new> job has me swamped. I've looked at your idea, and it does> seem solid for languages without side-effects (for example> Unimperative, or Joy or Haskell). For languages with> side-effects, then I don't see how we can practically> measure...

Chris,the provability of a type system is limited by the nature of the Turing machine. The halting problem proves that any algorithmic system can not be proven to terminate, and therefore a depentent type system is undecidable for all cases.A contracts system equals a type system where types are values, i.e. a depentent type system.A dependent...

Functional programming is a pain in the $$$. It will never catch on, because referential transparency gets in the way for most tasks, and programming around it using monads is the pain mentioned above.There is a huge misunderstanding currently going on about FP, and about Joel's comments. First of all, we have functional programming only when...

> The point of the article is not the example, but the idea.> The example is merely for illustration. These problems have been long solved in Fortran (the compiler automatically vectorizes loops), and in some functional languages.

> Is there truly such thing as provably correct code? Even> though some code can be proven to be correct with regards> to a specific specification, what guarantees that> specification to be correct? The solution and the> challenge go on ad infinitum without resolution. > > On the other hand code can be viewed as always correct, if> you take it...

> Well considering that you think deterministic implies> determinism, you are clearly confused. Determinism is a> philosophy:> http://www.google.com/search?hl=en&q=define%3A+determinismDeterminism is a word that in some contexts means 'a philosophy' and in some other contexts means 'deterministic state' as you described.> And therefore you...

> There is no proof that extra dimensions exist. It's just> an idea.Something has got to be hidden, because we haven't explained everything yet.At least you must admit to this simple truth.> As far as we can tell, at this point, yes this is the> case.No. There is nothing that suggest either this or the opposite view. There is no conclusive...

> You are not understanding the point of the discussion.> Whether software is deterministic doesn't have any> y bearing on the issue Bruce is talking about here.You are flamebaiting, but I won't bite. Let's keep the discussion on a good level.