On 6/2/07, Benjamin Goertzel <[EMAIL PROTECTED]> wrote:

http://www.singinst.org/research/summary

[see menu to the left] embodying some research I think will be extremely
valuable for pushing forward toward AGI, and that I think is well-
pursued in an open, nonprofit context.


* "Research Area 5: Design and Creation of Safe Software
Infrastructure" has enough support in the mainstream (industry and
academia) IMHO. Microsoft Research works on it; several little
companies are in this bussiness; every CompSci university department
has someone working on it. Feeling lucky with Google gives:
http://www.cs.utexas.edu/users/moore/publications/zurich-05/talk.html

Citing:

However, currently, there is no programming language that both
supports proof-based program correctness checking, and is sufficiently
efficient in terms of execution to be usable for pragmatic AGI
purposes.
<<

This is not how I would state things.  The burden is of course
efficiency of program development (proving program properties or
deriving program from specification) which is not much correlated (if
at all) with efficiency of the extracted/verified program. For
example, you can prove properties of assembly code (like in
dependently typed assembly languages).

-----
This list is sponsored by AGIRI: http://www.agiri.org/email
To unsubscribe or change your options, please go to:
http://v2.listbox.com/member/?member_id=231415&user_secret=e9e40a7e

Reply via email to