Invisible wrote:
> I wonder how many of these properties are decidable for "real-world" 
> programs...

There are many useful properties which are easy to determine, yes.

That you didn't violate the type system. That you didn't use a variable 
before you assigned to it. Etc.  However, most of those types of properties 
are restricted to the "I can prove you don't" versions, as mentioned earlier 
in the type system discussion.

Depending on the implementation language, it may be feasible to prove lack 
of deadlock, lack of livelock, compatibility between server and client, 
compatibility between two servers (i.e., a client that works with serverV1 
will also work with serverV2), and so on. However, it often gets very 
exponential very quickly, especially in more procedural vs functional 
languages.

-- 
   Darren New, San Diego CA, USA (PST)
   "We'd like you to back-port all the changes in 2.0
    back to version 1.0."
   "We've done that already. We call it 2.0."

Post a reply to this message