| |||||||||||||
Google's Native ClientGoogle's Native ClientPosted Jun 4, 2009 14:03 UTC (Thu) by NAR (subscriber, #1313)In reply to: Google's Native Client by Thue Parent article: Google's Native Client
Scientists also work on power plant based on nuclear fusion :-) I think that will be ready earlier than an automatic prover.
(Log in to post comments)
Google's Native Client Posted Jun 5, 2009 13:26 UTC (Fri) by Thue (subscriber, #14277) [Link]
Google already wrote the automatic prover. Now we just need to write the proof that the automatic prover is correct. Such a proof is written by hand with the current frontier science, and the proof is then checked by an automated proof validator.
I don't see anything here which is not already done today, just on a smaller scale.
Google's Native Client Posted Jun 10, 2009 15:26 UTC (Wed) by amarjan (guest, #25108) [Link]
What about implementation defects -- say in a given stepping of a particular CPU?
I'm not a low lever programmer so I can't site relevant examples from memory, but I know there have been numerous such defects with security implications over the years.
|
|||||||||||||