2009/1/22 Scott David Daniels <scott.dani...@acm.org>: > Having once been a more type-A, I labored for a couple of years trying > to build a restricted language that provably terminated for work on an > object-oriented database research.
I was careful to say that it was the /use/ of the language that is restricted; it's still possible to write undecidable programs, there's just an obligation on you to show that you haven't. > I finally gave it up as a bad idea, > because, in practice, we don't care if a loop will terminate or not in > database work; a transaction that takes a year to commit is equivalent > to an infinite loop for all applications that I have interacted with > (and yes, I have worked allowing four day transactions to commit). True -- the really serious safety critical stuff is usually real time, and part of the proof obligations is to show that the maximum response time is tolerable. The loop variant can help with that, too. -- Tim Rowe -- http://mail.python.org/mailman/listinfo/python-list
