Hi, As it happens that [safe software infrastructure] would not be anywhere near my top priority in staffing the Research Program.
My top priorities are -- AGISim -- Research Area 8: Cognitive Technologies If $$ can be raised to significantly fund these aspects, that will be a start.
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).
OK, I agree... that could have been worded better. But the fact remains that provably correct programming is not currently a pragmatic approach for AGI engineering. -- Ben G ----- 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
