From: Samantha Atkins (samantha@objectent.com)
Date: Sun Jun 13 2004 - 01:37:36 MDT
On Jun 12, 2004, at 8:02 AM, Ben Goertzel wrote:
> Of course, there's a possibility that a sufficiently smart NM system
> could find some kind of hole in the separation between layers -- a
> careful software bug. This leads to the need for specialized narrow-AI
> software focusing on program-correctness-checking, to verify that no
> such bugs exist. It also points to a problem in that the core is now
> implemented in C++, which isn't really very compatible with formal
> program verification technology. Therefore, for safety purposes, we'll
> need to reimplement the core in C# or Java. Doing a Java
> reimplementation when the time comes will not be extremely hard, since
> using gcc (the compiler we use), Java and C++ are compiled to the same
> sort of binaries. My friends at supercompilers.com have unique
> technology that allows formal verification of Java programs.
>
I don't see how "formal verification of Java programs" can be done. Or
at least, I would assume that the specification of what the program is
supposed to do is where much of the trick takes place. If the
specification is detailed enough and is itself provably correct (why
don't we get an infinite recurse?) then it might well be a better form
of the program than the Java one was anyway. The things Java removed
from C++ do not afaik make it any more powerful, certainly not more
succinct, and arguably no easier to prove a program is correct in. I
believe you can do this type of formalism for fairly small programs.
If it works for larger software systems then your friends should
practically own the server software space.
So how does this work? Is the core succinct enough to be formalized
into a proof engine? Or have the folks at supercompilers.com done
something that seems to me roughly equivalent to solving the halting
problem?
- samantha
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:47 MDT