Motivation Certify all code in a single type system/program logic? Hard to combine all features weak vs.strong update,functions/exceptions vs.goto's,threads vs. thread contexts May not be modular Very complex,hard to use Don't know how to design such a logic Certify modules using the most appropriate logic! Modules do not use all the features at the same time It is simpler to use specialized logic for each moduleMotivation ◼ Certify all code in a single type system/program logic? ◼ Hard to combine all features ◼ weak vs. strong update, functions/exceptions vs. goto’s, threads vs. thread contexts ◼ May not be modular ◼ Very complex, hard to use ◼ Don’t know how to design such a logic ◼ Certify modules using the most appropriate logic! ◼ Modules do not use all the features at the same time ◼ It is simpler to use specialized logic for each module