Trusted systems and SW
Real SW applications need quotation, inspection
Algorithms for solving problems will be very varied
Proof language can be very simple
Proof checker + digital signature verifier = secure agent
Small trusted code base
Tim Berners-Lee
32 of 35