From: Ben Goertzel (ben@goertzel.org)
Date: Sun Jun 13 2004 - 10:07:49 MDT
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.
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.
> 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.
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
> 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.
Well, we have big ambitions for supercompilers.com, which will more
likely be carried out via partnership with major software firms than by
competing directly with them. However, the technology is still in
development, and right now it works for SOME large software systems and
not others.
Specifically, if you design a software program with knowledge of the
supercompilation process in mind, then the program can be large and
complex and the supercompiler can still grok it. But if it's not
designed with supercompilation in mind, then the supercompiler may not
be able to do anything useful with it right now.
Hopefully, this limitation will be overcome. Even if not, however, it's
not such an obstacle for Novamente, because if we recode the Novamente
core in Java in future with supercompilation in mind, we can make sure
to structure the design in a supercompiler-friendly way.
> 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?
You don't need to solve the halting problem to prove that a program
successfully fulfills its specification, in most realistic cases. Yeah,
you can come up with cases where a program verifier will choke. But in
reality you can design a software system so that the program verifier
doesn't choke.
There is a LOT of knowledge in the area of formal program verification
and transformation, and plenty of cool academic-ish technology, even
though very little of this has found its way into the commercial
software community.
-- Ben G
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:47 MDT