programming languages the essence of computer scie

ProgrammingLanguages:TheEssenceofComputerScienceRobertHarperCarnegieMellonUniversityOctober,2002CSIsAboutProgramming•Howtobuildsystems.–Better,faster,cheaper.–Reliable,maintainable,extensible.•Evaluatingandcomparingsystems.–Performance,behavior,security.–Compliance,usability.•Whatcanandcan’tbedone.–Algorithmsandcomplexity.ProgrammingIsLinguistic•Programmingisanexplanatoryactivity.–Toyourself,nowandinthefuture.–Towhoeverhastoreadyourcode.–Tothecompiler,whichhastomakeitrun.•Explanationsrequirelanguage.–Tostateclearlywhatisgoingon.–Tocommunicateideasoverspaceandtime.ProgrammingLanguagesAreEssential•Thereforelanguagesareoftheessenceincomputerscience.–Programminglanguages,inthefamiliarsense.–Descriptionlanguages,designpatterns,architecturelanguages,specificationlanguages.SomeConventionalWisdom•PLresearchisover.–ThelanguageofthefutureisX…forvariousvaluesofX.–It’snotabouttheone,truelanguage!•AnyonecandesignaPL.–Clearly,anyonedoes.–Butlookwhatyouget!TCL,Perl,TeX,C++.•PLresearchisirrelevanttopractice.–Seenasapurelyacademicpursuit.–Butthetideisturningassuccessesaccumulate.SomeAccomplishments•High-levellanguages.•Statictypedisciplines.•Automaticstoragemanagement.•Objects,classes,ADT’s.•Sophisticatedcompilertechnology.•Specificationandverification.WhyPeopleDon’tNotice•Ittakesdecadestogofromresearchtopractice.–Similartootherareas,suchasalgorithms,AI.–Largeinstalledbaseofprogrammers.•Ideasbecome“commonsense”longbeforetheyarewidelyused.–Evenverysimplethings,suchaslexicalscope,wereoncecontroversial!–Nottomentiondataabstraction,OOP,….SomeImportantTrends•Safetywithperformance.–High-levellanguageswithgoodcompilers.–Low-levellanguageswithgoodtypesystems.•Languages,nottools.–Thedesignshouldlivewiththecode.–Conformanceshouldbecheckablethroughouttheevolutionofthecode.SomeImportantTrends•Interplaybetweentheoryandpractice.–“Provetheoremsandreportnumbers.”–Buildsystemstoassesspracticalityandtodiscovernewproblems.•Full-spectrumcoverage.–Functionalandimperative.–Highandlow-levellanguages.–Designandimplementation.SomeImportantTrends•TypetheoryastheGUTofPL’s.–Providesaprecisecriterionforsafetyandsanityofadesign.–“Features”correspondtotypes.–Closeconnectionswithlogicsandsemantics.WhatIsATypeSystem?•Staticsemantics:thewell-formedprograms.•Dynamicsemantics:theexecutionmodel.WhatisaTypeSystem?•Safetytheorem:typespredictbehavior.–Typesdescribethestatesofanabstractmachinemodel.–Executionbehaviormustcoherewiththesedescriptions.•Thusatypeisaspecificationandatypecheckerisatheoremprover.TypesAreSpecifications•Examples:–e:floatmeansthateevaluatestoavaluein,say,floatingpointregister0.–e:float!intmeansthateisaprocedurethatiscalledwitharginFR0andreturnswithresultinGR0.–e:queuemeansthatebehaveslikeaqueue.TypesAreFormalMethods•Typecheckingisthemostsuccessfulformalmethod!–Inprincipaltherearenolimits.–Inpracticethereisnoendinsight.•Examples:–Usingtypesforlow-levellanguages,sayinsideacompiler.–Extendingtheexpressivenessoftypesystemsforhigh-levellanguages.TypesinCompilation•Conventionalcompilers:Source=L1L2…Ln=Target:T1•Typesapplyonlytothesourcecode.–Typecheck,thendiscardtypes.–Ifcompileriscorrect,targetcodeissafe.TypedIntermediateLanguages•Generalizesyntax-directedtranslationtotype-directedtranslation.–Intermediatelanguagescomeequippedwithatypesystem.–Compilertransformationstranslatebothaprogramanditstype.–Translationpreservestyping:ife:Tthene*:T*aftertranslationTypedIntermediateLanguages•Type-directedtranslation:Source=L1L2…Ln=Target:::T1T2…Tn•Transferstypingpropertiesfromsourcecodetoobjectcode.–Checkintegrityofcompiler.–Exploittypesduringcodegeneration.CertifyingCompilers•Typesonobjectcodecertifyitssafety.–Typecheckingensuressafety.–Typeinformationensuresverifiability.•Examplesofcertifiedobjectcode:–TAL=typedassemblylanguage.–PCC=barecode+proofofsafety.–Manyvariationsarebeingexplored.TALExamplefact:8.{r1:int,sp:{r1:int,}::}jgzr1,positivemovr1,1retpositive:pushr1;sp:int::{t1:int,sp:}::subr1,r1,1callfact[int::{r1:int,sp:}::]imulr1,r1,r2popr2;sp:{r1:int,sp:}::retTypesforLow-LevelLanguages•Whatisagoodtypesystemforalow-levellanguage?–Shouldexposedatarepresentations.–Shouldallowforlow-level“hacks”.–Shouldbeverifiablysafe.–Shouldnotcompromiseefficiency.•Currentsystemsmakeseriouscompromises.–Veryweaksafetyproperties.–Forceatomicityofcomplexoperations.Example:MemoryAllocation•Mosttypesystemstakeanatomicviewofconstructors.–Allocateandinitializein“onestep”.–EvenHLL’slikeJavaimposerestrictions.•We’dliketoexposethe“finestructure”.–Supportcodemotionsuchascoalescing.–Allowincrementalinitialization.–Butneverthelessensuresafety!Example:MemoryAllocation•Anallocationprotocol(usedinTILT):–Reserve:obtainraw,un-initializedspace.–Initialize:assignvaluestotheparts.–Allocate:baptizeasavalidobject.•Currenttypesystemscannothandlethis.–Partiallyinitializedobjects.–In-placemodificationofparts.–Interactionwithcollectedheap.Example:MemoryAllocationHeapHPAP????LPAP120HPALow-LevelTypeSystem•Borrowtwoideasfromlinearlogic.–Restrictedandunrestrictedvariables.–Amodalitytom