nFormally,
the system meets its spec
oWe
have the theory needed to show this formally
oBut
doing it doesn’t scale
oAnd worse, we can’t get the formal spec right
▬Though we can get partial specs right
▬“Sorry, can’t find any more bugs.”
nInformally,
users aren’t surprised
oDepends
on user expectations
▬Compare 1980 AT&T with cellphones
▬How well does the market work for dependability?