From: Samantha Atkins (samantha@objectent.com)
Date: Sun Jun 13 2004 - 15:43:14 MDT
On Jun 13, 2004, at 9:07 AM, Ben Goertzel wrote:
>
> Hi,
>
>> 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.
>
> Formal specification may take place in a mathematical specification
> language such as Z. This is not a good form for a practical software
> program, because it doesn't deal with issues of memory or processing
> efficiency, except at the very abstract level of the
> order-of-complexity
> of algorithms and the design of data structures. Currently there is no
> technology for taking a Z specification and turning it into an
> efficient
> software program. However, the supercompiler technology may eventually
> lead to such a capability, in which case, indeed, the specification
> will
> be the program.
>
This is what I suspected. Unfortunately Z will not handle the POC of
the underlying mechanisms of Java/C##. It is precisely in those
mechanisms that unaddressed opportunities for failure or exploitation
of weaknesses are found.
> The point is that the specification is much smaller and simpler than a
> program, and hence can be more thoroughly checed my humans. We don't
> get an infinite recursion because the recursion stops with human
> judgment. The problem is that software programs that are too big and
> complex are hard for humans to reliably verify as correct by direct
> inspection.
>
So now sufficient POC to guarantee the SI will not take off and do
terrible things depends on humans reading and verifying a specification
of the intent of the programming? This doesn't look very "safe" to
me.
>> 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.
>
> This is not true. Java lacks pointers and explicit heap memory
> management, and this is what makes it orders of magnitude more feasible
> to analyze Java programs mathematically, than C++ programs. C#
> programs
> are tractable in the sense that Java programs are, if one doesn't use
> unsafe blocks of code and the pointer-manipulation that they permit.
>
What is not true? Mere pointer arithmetic and memory allocation being
out of the hands of programmers means that bugs in that stuff coded by
the application programmers will not eat your lunch. But it does not
mean there are no bugs in the underlying Java/C# implementation. It
also doesn't mean that the code itself is more easily proven correct
except in the narrow dimensions of pointers and memory management and
then only when we assume the correctness of the implementation. Most
of what programs are written for is outside these areas which are
simply means to some end. That end is no more verifiable than it was
before as actually being what the code will do in all possible
circumstances.
> The existing, partially functional Java supercompiler -- and the
> existing C# partial-evaluator made by the same team under a research
> grant from Microsoft -- could not have feasibly been made for C#.
I am not sure I parse your intent there.
>
>
- samantha
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:47 MDT