2.21

Se på engelsk

2.21 Typesystemer og statisk analyse

Overblik og motivation

De fleste fejl fanges sent, ved runtime, af en test eller en bruger eller en hændelse. En hel klasse af dem behøver aldrig nå så langt. Et typesystem og et godt værktøj til statisk programanalyse læser din kode, før den kører, og beviser, at visse fejl ikke kan ske: en streng brugt, hvor et tal kræves, en null dereferenceret, en variabel læst før den er skrevet, et tilfælde der er efterladt ubehandlet. Dette kapitel handler om at skubbe korrekthed mod venstre, tættere på det øjeblik, du skriver linjen, hvor en rettelse koster sekunder i stedet for en side i en hændelsesgennemgang.

Statisk analyse er enhver teknik, der undersøger kilde- eller kompileret kode uden at eksekvere den. Typekontrol er den mest udbredte form, men familien omfatter også linters (værktøjer, der markerer stilistiske og korrekthedsmønstre), dataflowanalysatorer og, i den fjerneste ende, formel verifikation. Det fælles løfte er en klasse af garantier, du får gratis ved hvert build, for evigt, uden at skrive en test og uden at nogen gennemgangere skal huske det. Det løfte er grunden til, at denne disciplin sidder ved siden af kodestandarder (kapitel 2.1), principper for softwaredesign (kapitel 2.2) og teststrategi (kapitel 2.4): det er endnu en automatiseret måde at gøre en stor kodebase sikker at ændre.

For store teams akkumuleres værdien. Når hundredvis af ingeniører rører et fælles system, er en typesignatur en kontrakt, som en compiler håndhæver over for hver enkelt af dem, og en kontrol i pipelinen er en gennemganger, der aldrig bliver træt og aldrig har favoritter. I virksomhedssammenhænge skærer dette omkostningen ved onboarding og integration, fordi typerne dokumenterer hensigt, og analysatorerne fanger de fejl, nyankomne begår. I offentlige og andre højrisikosystemer, hvor et forkert svar kan nægte en ydelse eller blotlægge data, er maskinkontrollerede garantier dokumentation: de viser en revisor, at hele kategorier af fejl er umulige ved konstruktion, ikke blot utestede. Dette hænger direkte sammen med softwarekvalitet (kapitel 2.11) og applikationssikkerhed (kapitel 4.2).

Grundprincipper

  • Skub korrekthed mod venstre: fang en fejl ved forfatningstidspunktet, ikke i produktion.
  • Foretræk garantier, maskinen kontrollerer, frem for konventioner, mennesker skal huske.
  • Kod hensigt ind i typer, så ulovlige tilstande slet ikke kan repræsenteres.
  • Adoptér typer gradvist i dynamisk kode; du behøver ikke alt eller intet.
  • Behandl advarsler som fejl, og ratchet baselinen, så den kun forbedres.
  • Kør de samme analysatorer i editoren og i pipelinen, med identiske regler.
  • Håndtér falske positiver med disciplineret, begrundet, gennemgåelig undertrykkelse.

Anbefalinger

Vælg statisk eller dynamisk typning med åbne øjne

I et statisk typet sprog kontrolleres typer, før programmet kører; i et dynamisk typet kontrolleres de, mens det kører, hvis overhovedet. Ingen af dem er universelt rigtig, og den ærlige ramme er en handel af garantier for fleksibilitet. Statisk typning køber dig maskinkontrollerede kontrakter, refaktorering du kan stole på, og værktøj (autofuldførelse, sikker omdøbning, hop-til-definition), der ved, hvad tingene er. Dynamisk typning køber dig hurtig prototyping, kortfattet kode og en lav ceremoni, der passer til scripts og udforskende arbejde. Jo større, mere langlivet og højere indsats systemet har, desto mere betaler den statiske side sig, fordi både omkostningen ved en refaktorering af hele kodebasen og omkostningen ved en runtime-typefejl vokser med skalaen.

Vær præcis om en anden, ortogonal akse: stærk versus svag typning. Et stærkt typet sprog nægter stiltiende at tvinge uforenelige typer (at lægge et tal til en streng udløser en fejl); et svagt typet konverterer stille og roligt og producerer overraskelser som "3" + 4, der giver noget, du ikke havde til hensigt. Du kan have statisk og svag, eller dynamisk og stærk. Når du evaluerer et sprog, så stil begge spørgsmål hver for sig, fordi “stærk” ofte er, hvad folk faktisk vil have, når de siger “typet.”

Støt dig til typeinferens for at holde typer billige

En almindelig indvending mod statisk typning er støjen ved at skrive en type på hver linje. Typeinferens fjerner det meste af den omkostning: compileren udleder typer fra konteksten, så du annoterer grænserne (funktionssignaturer, offentlige grænseflader) og lader det indre blive udledt. Moderne sprog udleder aggressivt og giver dig sikkerheden fra statisk kontrol med meget af kortheden fra dynamisk kode. Adoptér en husregel, der annoterer de dele, en læser støtter sig til som en kontrakt, de eksporterede funktioner og offentlige typer, og overlader lokale variabler til inferens. Det holder signaturer ærlige og selvdokumenterende, mens det skåner det indre for rod, og det knytter sig tilbage til læsbarhedsmålene i kapitel 2.1.

Gør ulovlige tilstande urepræsenterbare

Den mest kraftfulde idé i praktisk typedesign er at forme dine typer, så en forkert tilstand ikke kan skrives ned. Hvis en ordre enten er “kladde” uden betaling eller “afgivet” med en betaling, så modellér den ikke som én struct med nullable felter, hvor en kladde ved et uheld kunne bære en betaling, og en afgivet ordre kunne bære ingen. Modellér den som en sumtype (også kaldet en tagged union, discriminated union eller variant): en værdi, der er præcis én af et fast sæt former, hver med sine egne data. Nu findes de ugyldige kombinationer ikke, og kode, der håndterer værdien, må redegøre for hvert tilfælde, ellers klager compileren. Det forvandler et runtime-”bør aldrig ske” til et kompileringstids-”kan ikke ske”, hvilket er hele pointen.

Det samme instinkt driver flere hverdagsværktøjer. Brug en opregningstype i stedet for en magisk streng til et fast sæt tilstande. Pak en valideret værdi ind i en særskilt type (en EmailAddress frem for en nøgen streng), så “ikke-valideret input” og “valideret e-mail” er forskellige typer, compileren holder adskilt. Det er typesystemets udtryk for grænsevalideringsdisciplinen fra fejlhåndtering (kapitel 2.20): validér én gang ved kanten, konvertér til en type, der koder garantien, og lad det indre stole på den.

Tag nullbarhed og generics alvorligt

Nulpegeren, hvis opfinder kaldte den sin “milliard-dollar-fejl”, er den enkeltstående mest almindelige måde, et statisk typesystem plejede at lyve på: en værdi typet som en streng kunne i hemmelighed være null, og du fandt ud af det ved at crashe. Moderne typesystemer retter dette ved at gøre nullbarhed eksplicit. En værdi er enten en String, der aldrig er null, eller en Option/Maybe/nullable type, du skal pakke ud før brug, og compileren tvinger dig til at håndtere det tomme tilfælde. Hvis dit sprog tilbyder ikke-nullable typer eller en optional type, så brug dem overalt og behandl en nøgen nullable som en lugt. Det fjerner en hel slægt af produktionsnedbrud.

Generics, også kaldet parametrisk polymorfi, lader dig skrive kode, der virker over mange typer uden at opgive typesikkerhed: en List<T> er en liste af en bestemt type T, kontrolleret ved kompilering, frem for en liste af utypede ting, du caster og beder over. Ræk ud efter generics for at bygge genbrugelige containere, funktioner og abstraktioner, der forbliver stærkt typede. Parringen af sumtyper, ikke-nullable typer og generics er det, der lader et moderne typesystem udtrykke reelle domæneregler frem for blot at mærke primitiver.

Adoptér typer gradvist i eksisterende dynamisk kode

Du behøver ikke omskrive en dynamisk kodebase for at få typningens fordele. Gradvis typning lader typet og utypet kode sameksistere, så du tilføjer typer inkrementelt, hvor de betaler sig mest. Mange økosystemer understøtter nu dette direkte: typehints i Python kontrolleret af en separat typekontrollør, et typet supersæt, der kompilerer til et dynamisk sprog, eller typeannotationer lagt oven på en eksisterende runtime. Begynd ved grænserne og de mest kritiske moduler (pengekoden, sikkerhedskoden, datamodellen), slå kontrolløren til i en tilladende tilstand, og stram den over tid. Tilføj en regel om, at ny kode skal være typet, selv mens gammel kode indhenter. På nogle få kvartaler kan en stor utypet kodebase nå det punkt, hvor de fleste ændringer er typekontrolleret, og de dele, der betyder mest, er dækket først.

Kør linters, typekontrollører og dybere analysatorer sammen

Typekontrol er ét lag; tilføj de andre. Et lint-værktøj fanger mistænkelige mønstre, en typekontrollør ignorerer: en tildeling, der altid er sand, en ubrugt variabel, et gennemfald i en switch, en ressource der aldrig lukkes. Dybere analysatorer ræsonnerer om programmets adfærd. Dataflowanalyse sporer, hvordan værdier bevæger sig gennem koden, for at besvare spørgsmål som “bruges denne variabel nogensinde før den tildeles” eller “kan dette filhåndtag lække på en fejlsti.” Mange af disse værktøjer er bygget på abstrakt fortolkning, en teknik der kører programmet i det abstrakte over mængder af mulige værdier (for eksempel “positiv”, “nul” eller “negativ” i stedet for præcise tal) for at bevise egenskaber over alle eksekveringer på én gang, uden at køre nogen enkelt.

Nogle analysatorer sidder ved siden af sikkerhedsværktøj. Static application security testing (SAST) scanner kildekode for sårbarhedsmønstre som injektion, usikker deserialisering eller plettede data, der når en farlig sink, og den deler den dataflowmaskineri, der er beskrevet her; behandl den som en del af denne familie og koordinér den med applikationssikkerhed (kapitel 4.2). Den praktiske anbefaling er et lagdelt sæt: en hurtig linter til stil og åbenlyse fejl, en typekontrollør til kontrakter og én eller flere dybere analysatorer til de egenskaber, der betyder noget for dit domæne. Konfigurér dem fra versionsstyrede filer, så reglerne er de samme for alle.

Behandl advarsler som fejl, og ratchet baselinen

En advarsel, der ikke får bygget til at fejle, er en advarsel, der vil blive ignoreret. Når en log fyldes med hundredvis af tolererede advarsler, læser ingen den, og den ene, der betyder noget, gemmer sig i støjen. Adoptér en advarsler-som-fejl-politik, så en ny advarsel bryder bygget og bliver rettet i det øjeblik, det er billigst. På en legacy-kodebase med tusindvis af eksisterende advarsler kan du ikke vende den kontakt natten over, så brug en ratchet: registrér det nuværende antal som en baseline, bloker enhver ændring, der øger det, og driv det ned over tid. Baselinen kan kun falde. Det lader dig slå en streng regel til i dag uden en massiv oprydning på forhånd, mens det garanterer, at situationen aldrig bliver værre og støt bliver bedre.

Kobl analyse ind i editorer og CI, med hurtig feedback

Statisk analyse betaler sig mest, når feedbacken er øjeblikkelig. Kør de samme kontroller i editoren, gennem Language Server Protocol eller et tilsvarende, så en udvikler ser fejlen, mens vedkommende skriver, før de overhovedet gemmer. Kør derefter det identiske regelsæt i continuous integration (CI), så intet flettes uden at bestå, og bind dette ind i pipelinen fra kapitel 8.1. De to må være enige: hvis editoren er eftergivende og CI er streng, eller omvendt, mister folk tillid til begge. Hold analysen hurtig nok til at køre på hver ændring, cache resultater, og analysér kun det, der er ændret, hvor du kan, så kontrolløren er en hjælp frem for en skat. Når editor og pipeline håndhæver de samme regler på samme måde, holder standarden op med at være et dokument, folk glemmer, og bliver en egenskab ved miljøet.

Forbehold formel verifikation til den kode, der berettiger det

I den fjerneste ende af spektret ligger formel verifikation: matematisk at bevise, at et program opfylder en præcis specifikation, ikke blot at det består tests. Teknikker spænder fra modelcheck (udtømmende udforskning af et systems tilstande) til teorembevisning og afhængige typer (typer udtryksfulde nok til at kode fulde specifikationer). Dette er den dybeste garanti, der findes, og den dyreste at producere, så den fortjener kun sin plads, hvor en fejl er katastrofal, eller hvor certificering kræver det: kryptografiske biblioteker, flystyringskode, en hypervisor, en kritisk protokol. For det meste software er den rette investering stærke typer plus gode analysatorer, som fanger det meste af fordelen til en brøkdel af prisen. Vid, at formelle metoder (introduceret i kapitel 2.12) findes, og hvor grænsen går, så du griber til dem bevidst på den sjældne komponent, der har brug for dem.

Hold undertrykkelse ærlig

Ingen analysator er perfekt, og den disciplin, der skiller et betroet værktøj fra et ignoreret, er, hvordan du håndterer dets fejl. Ethvert seriøst værktøj lader dig undertrykke et fund. Kræv, at hver undertrykkelse er snæver (én linje eller ét fund, aldrig en hel fil eller regel), bærer en begrundelse i en kommentar og er synlig i gennemgang som enhver anden kode. Et generelt fravalg øverst i en fil er, hvordan dækning stille rådner. Revidér undertrykkelser periodisk og behandl en voksende bunke af dem som et signal om, at en regel er forkert kalibreret, eller at koden har et reelt problem, nogen skjuler. Ærlig undertrykkelse holder værktøjet troværdigt; tavs, gennemgribende undertrykkelse forvandler det til teater.

Afvejninger: fordele og ulemper

TilgangFordeleUlemper
Statisk typningMaskinkontrollerede kontrakter; sikker refaktorering; rigt værktøjMere ceremoni på forhånd; langsommere tidlig prototyping
Dynamisk typningHurtig at skrive; fleksibel; lav ceremoniTypefejl dukker op ved runtime; refaktoreringer er risikable
TypeinferensSikkerhed med korthed; mindre annotationsstøjUdledte typer kan sløre hensigt hvis overbrugt
Gradvis typningInkrementel adoption; dæk kritisk kode førstUtypede kanter lækker stadig; delvise garantier
Linters og dataflowanalyseFanger fejl, typer overser; billige at køreFalske positiver; støj hvis ukonfigureret
Advarsler-som-fejl med ratchetNye problemer blokeres; baselinen forbedres kunKan føles hindrende; kræver en undertrykkelsespolitik
Formel verifikationStærkeste garanti; beviser egenskaber for alle inputDyr, specialiseret; sjældent berettiget

Den tilbagevendende spænding er garantier versus gnidning. Hvert trin mod strengere typning og dybere analyse køber dig en klasse af fejl, der bliver umulige, og hvert trin tilføjer ceremoni, værktøjskøretid og den lejlighedsvise falske positiv, der koster en udvikler minutter. Løs det efter indsats og levetid. Et engangsscript eller en spike vil have den lette, hurtige, dynamiske ende. En betalingshovedbog, en tilladelseskontrol eller et system, en offentlig myndighed vil køre i femten år, vil have stærke typer, lagdelte analysatorer, advarsler-som-fejl og, til sin farligste kerne, måske formelt bevis. Afstem stringensen efter omkostningen ved at tage fejl, og lad inferens og gradvis adoption holde gnidningen overkommelig.

Spørgsmål til drøftelse med dit team

  1. Hvor i vores kodebase ville et typesystem have forebygget vores seneste produktionshændelser, og ved vi det? De fleste teams skændes om typning i det abstrakte, når dokumentationen sidder i deres egen hændelseshistorik. Træk de sidste ti eller tyve produktionsfejl og sortér dem: hvor mange var en null, hvor en værdi var forventet, en forkert form sendt over en grænse, et ubehandlet tilfælde, en strengtypet værdi, der drev? Det er netop de fejl, en typekontrollør og en linter fanger gratis. Hvis en stor del af jeres hændelser ligger i den kategori, har I et konkret, dollar-målt argument for stærkere typning i de moduler, hvor de skete. Hvis næsten ingen gør, bor jeres fejl andetsteds (logik, samtidighed, krav), og tungere typning er måske ikke jeres mest værdifulde træk. Uanset hvad erstatter I mening med data.

  2. Hvis vi adopterede gradvis typning, hvor ville vi begynde, og hvad ville “gjort nok” betyde? At slå en kontrollør til på tværs af en stor dynamisk kodebase er et program, ikke en kontakt, der vendes, og rækkefølgen afgør, om det lykkes eller går i stå. Drøft, hvilke moduler der bærer mest risiko (penge, autentificering, den centrale datamodel) og derfor fortjener typer først, versus hvilke der er stabile og har lav indsats nok til at blive utypet for nu. Aftal en regel for ny kode (typet fra dag ét), så den utypede flade holder op med at vokse, mens I hakker i bagsalden. Definér et mål: måske hver offentlig funktionssignatur typet, hver grænse valideret ind i en type, kontrolløren kørende i streng tilstand på de kritiske pakker. Uden en defineret målstreg bliver gradvis typning evig og halvdækket, hvilket er det værste af begge verdener.

  3. Hvad er vores politik, når en statisk analysator tager fejl, og holder den værktøjet troværdigt? Enhver analysator producerer falske positiver, og hvordan I håndterer dem, afgør, om værktøjet forbliver nyttigt eller bliver slået fra i frustration. Gå konkrete tilfælde igennem: når et fund er en ægte falsk positiv, er undertrykkelsen så snæver, kommenteret med en begrundelse og synlig i gennemgang, eller slår nogen hele reglen fra for hele repositoriet? Se på jeres nuværende undertrykkelser: hvor mange er der, bærer de begrundelser, og hvornår reviderede nogen dem sidst? En bunke uforklarede, brede undertrykkelser betyder, at jeres dækning er stille hul. Målet er en fælles, håndhævet disciplin, der holder analysatoren troværdig, så dens fund stoles på og handles på frem for refleksivt gjort tavse.

  4. Hvilke sprog og analysatorer standardiserer vi på, og hvordan holder vi ét regelsæt, efterhånden som vores stak fragmenterer på tværs af teams? Når hundredvis af ingeniører arbejder i flere sprog, ødelægger det stille garantien, hvis hvert team driver til sin egen kontrollør, sine egne lintregler og sin egen strenghedsindstilling, fordi en kontrakt håndhævet i ét repositorium blot er et forslag i det næste. Det modstridende træk er reelt: central standardisering giver jer flytbare ingeniører og ensartet revisionsdokumentation, men et regelsæt pålagt fra centrum kan kæmpe mod et sprogs idiomer eller sinke et team, der havde gode grunde til sin egen konfiguration. Tag en opgørelse med over sprogene i produktion, de analysatorer og versioner hvert team kører, og en diff af deres regelsæt, så driften er synlig frem for antaget. I en virksomheds- eller offentlig sammenhæng så bind svaret til indkøb og revision: en enkelt versionsstyret konfiguration, hvert repositorium arver, er det, der lader en revisor bekræfte, at de samme kontroller kørte overalt, og det er det, der stopper en leverandør i at levere kode under svagere regler, end jeres eget personale skal opfylde.

  5. Hvor hurtig er vores analyse, og på hvilket punkt begynder folk at omgå den? En kontrollør er kun en garanti, hvis den kører på hver ændring, og i det øjeblik den gør rediger-byg-løkken smertefuld, lærer ingeniører at springe den over, slå den fra lokalt eller flette med den rød og love at rette den senere. Spændingen er dybde versus hastighed: en dybere dataflow- eller sikkerhedspas finder fejl, en hurtig linter overser, men hvis hele suiten tager tyve minutter, holder folk op med at vente på den, og en kontrol, ingen venter på, beskytter ingenting. Tag de reelle tal med til drøftelsen: editorfeedbackens latens, CI’s vægurstid for analysetrinnet, cache-hitrater, hvor ofte builds flettes med kontroller sprunget over eller tilsidesat, og hvor stor en del af kørslen der er inkrementel versus fuld. For en stor eller offentlig organisation så tilføj regnebudgettet og gennemløbsomkostningen, fordi et langsomt obligatorisk analysetrin i flådeskala både er en budgetpost og en kø, der forsinker hver udgivelse, og den ærlige rettelse er som regel inkrementel analyse og caching frem for stille at lempe reglerne.

  6. Hvilken maskinkontrolleret dokumentation kan vi faktisk producere til en revisor, og hvilke af vores kritiske invarianter dækker den? I regulerede og højrisikosystemer er pointen med typning og statisk analyse påviselig dokumentation for, at hele klasser af fejl er umulige ved konstruktion, ud over de hverdagsfejl, den forebygger, og den påstand er værdiløs, hvis I ikke kan vise, hvilke invarianter der håndhæves, og hvor. Afvejningen er omfang mod omkostning: at bevise mere (ikke-nullbarhed overalt, sumtyper for hver lovlig tilstand, formel verifikation af kerneberegningen) køber stærkere dokumentation, men hvert trin opad i stringens koster annotationsindsats, specialisttid og buildkompleksitet, I måske ikke har brug for på kode med lav indsats. Tag et kort med over jeres sikkerhedskritiske moduler til de garantier, hvert i øjeblikket bærer, listen over åbne undertrykkelser med deres begrundelser og eventuelle huller, hvor en kritisk regel håndhæves af konvention frem for compileren. For en offentlig eller reguleret virksomhed så ram dette ind som certificeringsdokumentation: en revisor bør kunne spore en påkrævet egenskab til en maskinkontrolleret type eller et bevis og se undertrykkelsesloggen, der dokumenterer hver undtagelse, så compliance hviler på artefakter, værktøjskæden genererer, frem for på manuel gennemgang bagefter.

Sektorperspektiv

Startup. Hastighed vinder, så ræk ud efter den billigste sikkerhed, der ikke sinker dig: et stærkt typet sprog eller en typekontrollør i tilladende tilstand, plus en hurtig linter i editoren, og typér din penge- og autentificeringskode først. Spring formel verifikation og dybe dataflowsuiter helt over; de koster tid, du ikke har. Den gevinst, du vil have tidligt, er en refaktorering, du kan stole på ved ti tusind linjer, så slå kontrolløren til, før kodebasen er for stor til at tæmme.

Lille virksomhed. Uden en specialist i statisk analyse på stat så foretræk et sprog og en værktøjskæde, hvor gode standarder er indbygget, frem for en suite, du skal justere og passe. Køb analysen indlejret i din IDE og din hostede CI i stedet for at opstille din egen platform, og hold regelsættet tæt på fællesskabsstandarden, så en konsulent eller en nyansat genkender det. Behandl advarsler-som-fejl og en lille typet kerne som de træk med størst løftestang, dit begrænsede budget kan foretage.

Stor virksomhed. Arbejdet er styring på tværs af mange teams: én versionsstyret konfiguration, hvert repositorium arver, identiske regler i editoren og pipelinen og en ratchet baseline, så intet teams dækning stille kan falde. Standardisér analysatorerne, følg typedækning og antal undertrykkelser som porteføljemålinger, og revidér undertrykkelser efter en fast kadence, så maskinkontrollerede garantier forbliver ensartede nok til, at en revisor kan stole på dem. Budgettér platformsteamet, der ejer den fælles konfiguration, fordi ensartethed på tværs af tusindvis af ingeniører ikke vedligeholder sig selv.

Offentlig sektor. Indkøb, åbenhed og lange levetider dominerer. Kræv i kontrakter, at leverandører opfylder de samme analyseregler, jeres eget personale gør, og afleverer konfigurationen og undertrykkelseslogge som leverancer, så garantien overlever et leverandørskifte. Foretræk maskinkontrolleret dokumentation frem for manuel sikring for berettigelses- og betalingslogik, forbehold formel verifikation til de beregninger, hvis fejl ville nægte en ydelse ulovligt, og hold hver undertrykkelse dokumenteret til revision gennem det årti eller mere, systemet vil køre.

Eksempler

Startup. Et startup med seks medarbejdere bygger sit produkt i et dynamisk sprog for hastighedens skyld, hvilket tjener dem godt, indtil en refaktorering ved ti tusind linjer begynder at forårsage runtime-typefejl, de kun finder i produktion. De adopterer gradvis typning: de slår en typekontrollør til i tilladende tilstand, tilføjer typehints til deres centrale domænemodel og betalingskode først og sætter en regel om, at alle nye moduler skal være fuldt typet. De kobler kontrolløren og en linter ind i deres editor og CI med identisk konfiguration og behandler nye advarsler som fejl, mens de ratchet’er de eksisterende ned. På to kvartaler forsvinder nedbrud fra uoverensstemmende former, refaktorering holder op med at være skræmmende, og en nyansats autofuldførelse ved faktisk, hvad hver funktion returnerer. Investeringen kostede nogle få ingeniøruger og fjernede en tilbagevendende kilde til kundevendte fejl.

Stor virksomhed. En global bank standardiserer statisk analyse på tværs af tusindvis af ingeniører. Hvert repositorium arver en fælles konfiguration: en typekontrollør i streng tilstand, en linter, en dataflowanalysator og en SAST-scanner til sikkerhedsmønstre, alle kørende i editoren og håndhævet i pipelinen, så intet flettes uden at bestå. Domænetyper gør ulovlige tilstande urepræsenterbare i den kode, der flytter penge: en bogført transaktion og en afventende er forskellige typer, valutaer er typet, så man ikke kan lægge dollars til euro, og validerede input er særskilte typer fra rå. Advarsler er fejl, og hvert teams baseline kan kun falde. Undertrykkelser kræver en begrundelse og revideres kvartalsvis. Fordi garantierne er maskinkontrollerede og ensartede, kan revisorer se, at hele klasser af fejl er umulige ved konstruktion, og ingeniører bevæger sig trygt på tværs af ukendte tjenester.

Offentlig sektor. En national skattemyndighed moderniserer et ydelsesberegningssystem, der skal være korrekt og forklarligt i årevis. Den centrale berettigelseslogik er skrevet i et stærkt typet sprog, hvor domænemodellen koder reglerne: en ansøgers status er en sumtype, der dækker hvert lovligt tilfælde, pengebeløb er en dedikeret type, der ikke kan forveksles med antal, og ingen værdi, der kunne mangle, efterlades som en nøgen nullable. Statisk analyse kører i CI som en port, og det mest sikkerhedskritiske beregningsmodul kontrolleres desuden med formelle metoder for at bevise, at nøgleinvarianter holder for alle input, hvilket opfylder certificeringskrav. Hver undertrykkelse er dokumenteret til revision. Når de oprindelige forfattere går videre, arver deres efterfølgere kode, hvis kontrakter compileren håndhæver, så de kan ændre den sikkert et årti senere.

Business case: motivation, ROI og TCO

Afkastet af typning og statisk analyse er et skift i, hvor du betaler for fejl. En fejl fanget af en typekontrollør i editoren koster sekunder; den samme fejl fanget i produktion koster en hændelse, en undersøgelse, muligvis kundeskade og et regulatorisk fund. Undersøgelser af fejløkonomi viser konsekvent omkostning, der stiger med en størrelsesorden for hvert trin, en fejl overlever, fra forfatning til gennemgang til test til produktion. Statisk analyse flytter en hel kategori af fejl til det billigste trin, ved hvert build, uden arbejde pr. fejl. Det er en fast, for det meste engangs opsætningsomkostning, der køber en ubegrænset strøm af forebyggede fejl, hvilket er tæt på den bedste løftestang i ingeniørarbejde.

Omkostningerne er reelle, men beskedne og forudbetalte. I vælger og konfigurerer værktøjerne, I betaler noget ceremoni i annotationer (blødgjort af inferens), I bruger ingeniørtid på at adoptere gradvis typning i legacy-kode, og I accepterer lejlighedsvise falske positiver. Sæt det over for de totale ejeromkostninger ved alternativet: hver typeformet fejl, der når produktion, hver risikabel refaktorering undgået, fordi intet garanterer korrekthed, hver langsom onboarding, fordi koden ikke dokumenterer sine egne kontrakter, og i regulerede sammenhænge hver revision, der skal tilfredsstilles ved manuel gennemgang frem for maskinkontrolleret dokumentation. For at argumentere over for ledelsen, bind det til de målinger, de allerede følger: andel fejlslagne ændringer, andel undsluppne fejl, middeltid til genopretning og andelen af hændelser, der kan tilskrives forebyggelige type- og nullfejl. Den graf, der overbeviser folk, er jeres egen hændelseshistorik sorteret efter, om en kontrollør ville have fanget den.

Anti-mønstre og faldgruber

  • Flugtlugen som vane: at caste til any, dynamic eller det utypede ækvivalent for at gøre kontrolløren tavs, hvilket udsletter garantien netop, hvor du havde mest brug for den.
  • Strengtypet alt: at sende nøgne strenge og utypede maps over grænser i stedet for at modellere tilstande som reelle typer, så compileren ikke kan hjælpe.
  • Nullable som standard: at lade værdier være nullable, når sproget tilbyder ikke-nullable og optional typer, og bevare milliard-dollar-fejlen.
  • Advarsler, der aldrig fejler: tusindvis af tolererede advarsler, hvori den, der betyder noget, er usynlig, fordi intet nogensinde bryder bygget.
  • Editor og CI er uenige: eftergivende lokalt og strenge i pipelinen, eller omvendt, så udviklere mistror begge, og flet overrasker folk.
  • Generel undertrykkelse: at slå en hel regel eller fil fra i stedet for ét begrundet fund, hvilket stille udhuler dækningen.
  • Analyseteater: at køre værktøjer, hvis fund ingen læser eller handler på, så rapporterne hobes op, og værdien er nul.
  • Alt-eller-intet-typning: at nægte at starte, fordi man ikke kan typere alt på én gang, og gå glip af de store gevinster ved at typere den kritiske kode først.
  • Verifikation overalt: at række ud efter formelle metoder på almindelig kode og bruge knap specialistindsats, hvor stærke typer ville have rakt.

Modenhedsmodel

  • Niveau 1, Opstart: Typning og analyse er ad hoc og pr. udvikler. Dynamisk kode har ingen kontrollør, eller et statisk sprog kører med ignorerede advarsler. Typeformede fejl (nulls, forkerte former, ubehandlede tilfælde) når produktion regelmæssigt, og refaktorering frygtes, fordi intet verificerer korrekthed.
  • Niveau 2, Udvikling: En linter og, hvor relevant, en typekontrollør kører på nogle projekter, men regler varierer mellem teams, advarsler får ikke bygget til at fejle, og flugtlemme og brede undertrykkelser er almindelige. Noget gavn realiseres, men dækningen er inkonsistent, og tilliden til værktøjerne er pletvis.
  • Niveau 3, Standardisering: En fælles, versionsstyret konfiguration håndhæver typekontrol og linting i editor og CI med identiske regler i hele organisationen. Advarsler er fejl med en ratchet baseline, nullbarhed og sumtyper bruges til at gøre ulovlige tilstande urepræsenterbare ved grænser, og hver undertrykkelse kræver en dokumenteret, gennemgåelig begrundelse.
  • Niveau 4, Styring: Analyse måles og styres mod baselines. Typedækning på kritiske moduler, antal advarsler, rater for falske positiver, antal undertrykkelser og andelen af produktionshændelser, en kontrollør ville have fanget, følges mod eksplicitte mål. Målingerne lukker porte for ændring: dækning på penge- og autentificeringskoden kan ikke falde, en stigende rate af falske positiver udløser omkalibrering af regler, og dashboards viser, om garantierne faktisk holder frem for blot er konfigureret.
  • Niveau 5, Orkestrering: Analyse forbedres løbende og er integreret i hele organisationen. Gradvis typning har nået de kritiske moduler, dataflow- og sikkerhedsanalysatorer kører rutinemæssigt, regler tilpasser sig, efterhånden som sprog og trusler udvikler sig, og formel verifikation anvendes bevidst på de få komponenter, hvis fejl ville være katastrofal. Værktøjet, målingerne og regelsættet føder tilbage i design, ansættelse og indkøb, så hele organisationen bliver støt sikrere at ændre.

Idéer til drøftelse

  1. Hvilke af jeres seneste produktionsfejl ville en typekontrollør eller linter have fanget, og hvilken andel af det samlede antal repræsenterer de?
  2. Hvor i jeres domænemodel kunne en sumtype eller en valideret indpakningstype forvandle et runtime-”bør aldrig ske” til et kompileringstids-”kan ikke ske”?
  3. Hvis I forvandlede advarsler til fejl i morgen, hvor mange ville bryde bygget, og hvilken baseline og ratchet ville lade jer adoptere politikken uden et oprydningskorstog?
  4. Kører jeres editor og jeres pipeline nøjagtig de samme regler, og hvordan ville en udvikler finde ud af, hvis de var drevet fra hinanden?
  5. Hvor mange undertrykkelser bor der i jeres kodebase lige nu, hvor mange bærer en begrundelse, og hvornår blev de sidst revideret?
  6. Er der nogen komponent i jeres system, hvis fejl er katastrofal nok til at berettige formel verifikation, og hvordan ville I vide det?

Vigtigste pointer

  • Statisk typning og analyse skubber en hel klasse af fejl til det billigste øjeblik at rette dem: mens du skriver koden, ved hvert build, uden arbejde pr. fejl.
  • Foretræk garantier, maskinen kontrollerer, frem for konventioner, mennesker skal huske, og kod hensigt ind i typer, så ulovlige tilstande slet ikke kan repræsenteres.
  • Du behøver ikke alt eller intet: gradvis typning lader dig dække den kritiske kode (penge, autentificering, datamodellen) først, mens resten indhenter.
  • Behandl advarsler som fejl med en ratchet baseline, kør identiske regler i editoren og CI, og hold undertrykkelse snæver, begrundet og revideret.
  • Afstem stringens efter indsats: stærke typer plus lagdelte analysatorer til de fleste systemer, og formel verifikation forbeholdt den sjældne komponent, hvis fejl er katastrofal.

Referencer og videre læsning

  • Benjamin C. Pierce, Types and Programming Languages
  • Simon Peyton Jones (ed.), The Implementation of Functional Programming Languages
  • Flemming Nielson, Hanne Riis Nielson, and Chris Hankin, Principles of Program Analysis
  • Patrick Cousot and Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”
  • Scott Wlaschin, Domain Modelling Made Functional
  • Steve McConnell, Code Complete: A Practical Handbook of Software Construction
  • Michael Barr and the MISRA Consortium, MISRA C: Guidelines for the Use of the C Language in Critical Systems
  • Al Bessey et al., “A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World,” Communications of the ACM