On 2007-08-31, Ricardo Aráoz <[EMAIL PROTECTED]> wrote: > Russ wrote: >> Yes, thanks for reminding me about that. With SPARK Ada, it is >> possible for some real (non-trivial) applications to formally >> (i.e., mathematically) *prove* correctness by static analysis. >> I doubt that is possible without "static declarative type- >> checking." >> >> SPARK Ada is for applications that really *must* be correct or >> people could die. > > I've always wondered... Are the compilers (or interpreters), > which take these programs to machine code, also formally proven > correct? And the OS in which those programs operate, are they > also formally proven correct? And the hardware, microprocessor, > electric supply, etc. are they also 'proven correct'?
Who watches the watchmen? The contracts are composed by the programmers writing the code. Is it likely that the same person who wrote a buggy function will know the right contract? -- Neil Cerutti The third verse of Blessed Assurance will be sung without musical accomplishment. --Church Bulletin Blooper -- http://mail.python.org/mailman/listinfo/python-list
