From: Ben Goertzel (ben@goertzel.org)
Date: Thu Sep 08 2005 - 05:52:03 MDT
Mikko,
You're right of course that I spoke sloppily, one of my numerous bad habits
;-)
What I meant, when I referred to "program correctness checking," was really
"program verification" in the sense of "formally verifying that a program
has certain properties of interest."
For starters, this means something along the lines of Programatica
http://www.cse.ogi.edu/~hallgren/Programatica/HW2003/demoabstract.html
a Haskell framework which supports three basic forms of evidence regarding
claims about Haskell programs:
-- informal claims (``I say so'')
-- tests run with a tool called QuickCheck
-- formal proofs done using a theorem-prover called Alfa
This framework allows one to formally prove *some* rigorous and interesting
statements about Haskell programs.
Relatedly, Bill Harrison's work
http://www.cs.missouri.edu/~harrison/pubs/research/research.html
(see particularly the paper "Domain Separation by Construction") uses monads
to allow one to prove formally that Haskell programs are "safe" in certain
senses. For instance, if one produces a program with two different modules
that don't interact (even though they share the same memory space), his
formalism lets one prove -- even in complex cases -- that they truly don't
and can't interact. This allows one, in theory, to combine safety with
efficiency in many cases (though of course this efficiency is only
theoretical at the moment as there is no efficient Haskell compiler!).
This general kind of approach to security of software would seem to be a
prerequisite to safe AGI. Without it, it's hard to be sure that bugs in
one's software aren't preventing one's supposedly "Friendly" architecture
from actually being Friendly.
Research in automated verification of appropriate properties of computer
programs, including safety-related properties, COULD proceed alongside
research in AGI ---- in some ideal world where AGI and functional
programming were adequately-funded domains of endeavor....
-- Ben
> On Wed, 7 Sep 2005, Ben Goertzel wrote:
> > 6) automatic program-correctness-checking integrated with above system
>
> > And, achieving 3-6 remains far off, and involves a lot of work. 4 is
> > of course straightforward work, and 6 is straightforward though subtle,
> > but 3 is quite subtle and involves a lot of
> > tricky computer science as well as difficult programming.
>
> Actually depending on what you mean by automatic
> program-correctness-checking, it may not be simple, nor straightforward.
>
> Automatic program verification for correctness is as a general task
> impossible, because in general case it is impossible to tell whether two
> Turing machines are equivalent or not. Still, there are people working on
> tools that are capable of verifying quite many things even from written
> code such as impossibility of getting into a deadlock, or livelock,
> etc.
>
> If you mean whether the compiler or some such verifies that the
> program is
> a legal example of the programming language (as for example c and most
> other often used languages do), then you are quite right. The task is
> quite straightforward and a small amount of understanding of programming
> and theory of computation should allow one to do the job.
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:52 MDT