[cap-talk] Avoid overconfidence (was: Any hope in RSA 2008?)

[Toby Murray]

On Sat, 2008-04-05 at 08:00 -0700, Mark Miller wrote:
> I remain
> hopeful that further work on formal tools, like Fred's SCOLL and
> Toby's Authodox, may bring these costs down much farther. But I also
> remain skeptical. Formal tools for assuring program correctness have
> been three weeks away for the last forty years.
> 

Just like the widespread deployment of capability-based systems that
solve real world problems ;)

(No this isn't a flame. I'm a strong believer in the virtues of both
formal methods and capabilities. It's just ironic. I hope to see both
"arrive".)

I'm pretty sure Peter Neumann of PSOS fame (one of the first efforts to
build a formally verified capability-based OS) has somewhere paraphrased
the "capabilities are the way of the future and always will be" as
"formal methods are the way of the future and always will be", in order
to note that both are promising technologies that have yet to properly
deliver.