On 08/10/2012 10:05 AM, "Franciszek Czekała" <[email protected]>" wrote:
The program was written with Ada and failed in a most stupid way. Is it not a proof enough that safety cannot be sensibly enforced by mechanical tools?
It only shows that Ada cannot provide such safety guarantees. (Which is clear from its specification alone, there actually was no need to blast a rocket to establish that fact.) It is perfectly possible that automated reasoning will become strong enough to automatically prove some interesting program properties.
