🇨🇿 Proč si IOG vybrala Haskell pro budování Cardano?

Tým IOG se pečlivě rozhodoval, který programovací jazyk a nástroje pro vývoj Cardana použije. Nakonec se rozhodli pro Haskell. Tým musí být schopen formálně ověřit, že vše, co je napsáno ve white paperech (bílých knihách), bude správně odpovídat zdrojovému kódu. Pojďte si přečíst, jak tým převádí matematické důkazy z white paperů do zdrojového kódu Haskellu.

TLDR

  • Před Cardanem žádný projekt z první desítky nepoužíval formální metody.
  • White paper je základem pro formální specifikaci. Ta je základem pro zdrojový kód napsaný v jazyce Haskell.
  • Formální specifikace a zdrojový kód v jazyce Haskell mají velmi podobný zápis.

Od white paperu ke zdrojovému kódu

Mnoho týmů v blockchainovém odvětví má mentalitu startupů “rychle kupředu za cenu rozbíjení věcí po cestě”. Tato mentalita je poháněna mládím, chamtivostí a vášní. Zdrojový kód mnoha protokolů je často psán ve spěchu a bez předchozího výzkumu. V některých případech můžeme hovořit o nezodpovědném přístupu týmů k uživatelům. Protikladem je pomalý, metodický a akademicky orientovaný přístup motivovaný snahou o upevnění inovací v našem prostoru. V době, kdy tým začal vyvíjet Cardano, nebyla žádná z deseti největších kryptoměn podle tržní kapitalizace založena na studiích, které nezávisla posoudil někdo jiný a nebyla implementována na základě formální specifikace. Tým IOG se rozhodl využívat formální metody pro vývoj Cardano.

Tým IOG definuje a matematicky dokazuje správnost chování protokolu a dalších komponent v bílých knihách. Ty jsou pak použity k vytvoření formální specifikace. Formální specifikace je přesný matematický popis chování a vlastností systému.

V bílých knihách se k vyjádření abstraktních pojmů a matematických důkazů používá matematický zápis. To je přesné, ale pro neodborníky může být obtížně srozumitelné. Zápis formální specifikace se používá k vyjádření chování a vlastností softwarového systému přesným, matematickým způsobem. Je méně abstraktní než matematický zápis, ale přesnější než zdrojový kód. Jinými slovy, programátor nemusí rozumět matematickému zápisu používanému v bílých knihách, ale je schopen porozumět formální specifikaci.

Po vytvoření formální specifikace je dalším krokem implementace zdrojového kódu v programovacím jazyce Haskell. Očekává se, že implementace bude dodržovat specifikace a vlastnosti popsané ve formální specifikaci. Implementace by měla být provedena tak, aby bylo možné matematicky dokázat, že implementace splňuje požadavky a vlastnosti popsané ve formální specifikaci. Jinými slovy, zdrojový kód lze formálně ověřit na základě specifikace.

K vyjádření implementace Cardana se používá zdrojový kód jazyka Haskell. Jedná se o nejkonkrétnější formu očekávaného chování. Je to forma, ve které je systém spuštěn. Zdrojový kód jazyka Haskell je méně přesný než formální zápis specifikace, ale vývojáři jazyka Haskell mu lépe rozumí.

I když existuje vztah mezi matematickým zápisem, zápisem formální specifikace a zdrojovým kódem Haskellu, není vždy snadné mezi nimi přepínat. Úroveň abstrakce a vyjadřovací schopnosti každého z nich je jiná, protože se používají různé notace. Cílem je maximalizovat přenos informací mezi různými notacemi.

Vědci a matematici nemusí být nutně programátory v Haskellu. Jejich úkolem je napsat bílou knihu. Programátoři Haskellu nemusí být špičkoví matematici. Formální specifikace je jakýmsi prostředníkem mezi těmito dvěma skupinami. Musí existovat někdo, kdo je schopen vytvořit formální specifikaci z bílé knihy. Je však možné použít nástroje, které dokáží automaticky překládat mezi matematickým zápisem, zápisem formální specifikace a zdrojovým kódem, například závislostně typované programovací jazyky jako Coq nebo Agda.

Cog i Agda jsou formální verifikační nástroje, které lze použít v kontextu funkcionálních programovacích jazyků, jako je Haskell. Oba jsou asistenti důkazů, což jsou počítačové programy, které pomáhají uživatelům psát formální matematické důkazy.

Cog i Agda jsou založeny na myšlence využití formálních metod ke zvýšení spolehlivosti a správnosti softwarových systémů. Zatímco Cog je specifičtější pro souběžné algoritmy, Agda je obecnější a lze ji použít pro jakýkoli druh funkcionálního programování. Oba jsou výkonnými nástroji pro zajištění správnosti softwarových systémů a lze je použít společně, aby poskytly komplexní řešení pro verifikaci.

Proč právě Haskell

Haskell je funkcionální programovací jazyk, který se dobře hodí pro použití formálních metod při vývoji softwaru.

Jednou z hlavních výhod jazyka Haskell je jeho silný typový systém. Haskell má statický typový systém, což znamená, že typy jsou kontrolovány při kompilaci, což zajišťuje vysokou úroveň bezpečnosti a zabraňuje mnoha typům chyb ještě před spuštěním programu. Haskell navíc podporuje typovou inferenci, což znamená, že programátor nemusí explicitně specifikovat typy proměnných a funkcí, takže kód je stručnější a čitelnější.

V jazyce Haskell jsou proměnné ve výchozím nastavení neměnné, což znamená, že jakmile je proměnné přiřazena hodnota, nelze ji změnit. To usnadňuje uvažování o chování programu a může zjednodušit souběžné a paralelní programování. Nezměnitelnost také pomáhá předcházet chybám způsobeným neočekávanými změnami proměnných a také umožňuje lepší testování kódu.

Jazyk Haskell je také silně zaměřen na funkcionální programování, které podporuje deklarativní a expresivní styl programování. Ve funkcionálním programování je kladen důraz na popis toho, co má program dělat, a ne na to, jak to má dělat. Díky tomu je kód čitelnější a lépe udržovatelný a může zjednodušit ladění a testování.

Díky silnému typovému systému a matematickému stylu programování se jazyk Haskell přirozeně hodí pro formální metody. Typový systém v jazyce Haskell je velmi expresivní a umožňuje vysokou úroveň statické kontroly kódu. To znamená, že mnoho běžných programátorských chyb lze zachytit již při kompilaci, nikoli až za běhu. Paradigma funkcionálního programování navíc podporuje matematický styl myšlení, což přispívá k větší předvídatelnosti kódu a jeho snadnějšímu zdůvodňování. To může být zvláště výhodné pro složité a rozsáhlé kódové báze Cardano.

Haskelovský garbage collection a striktní vyhodnocování zajišťují, že program je chráněn před chybami za běhu, jako jsou dereference nulových ukazatelů, přetečení bufferu a datové závody. Díky tomu je vhodnější pro systémy kritické z hlediska bezpečnosti.

Model souběžnosti a paralelismu jazyka Haskell je založen na lehkých vláknech a předávání zpráv, což usnadňuje psaní kódu, který může využívat více jader a procesorů. To je důležité pro projekt Cardano, což je blockchainová platforma, která musí zpracovávat velké množství transakcí současně.

Vysokoúrovňové abstrakce jazyka Haskell, jako jsou monády, usnadňují psaní kódu, který je modulární, složitelný a opakovaně použitelný. To může pomoci snížit složitost kódové základny a usnadnit zdůvodňování a dokazování vlastností kódu.

Faktoriál funkce

Pojďme se podívat na jednoduchý příklad jak se může matematický zápis transformovat do zdrojového kódu.

Úplný matematický důkaz funkce faktoriál by vypadal asi takto:

Podívejte se na formální specifikaci faktoriál funkce v notaci Agda:

Podívejte se na formální specifikaci faktoriál funkce v notaci Coq:

Podívejte se, jak se zdrojový kód funkce factorial v jazyce Haskell podobá notaci Agda a Coq:

Pro srovnání se podívejte, jak vypadá implementace funkce faktoriál v tradičním jazyce C++:

Programátor musí rozumět formální specifikaci, aby byl schopen napsat odpovídající zdrojový kód v jazyce Haskell. Programátor může samozřejmě napsat funkci faktoriál i v jazyce C++, ale všimněte si, že zápis je méně podobný formální specifikaci. Kód v obou případech dělá přesně to, co podle specifikace dělat má, což je ze všeho nejdůležitější.

Pro programátora je však přirozenější porovnávat notaci jazyka Haskell a formální specifikaci, než kdyby měl totéž dělat s jazykem C++ (nebo jiným podobným jazykem). Rozdíl by byl patrnější u složitějších funkcí.

Závěr

Tým IOG měl pro volbu jazyka Haskell mnoho důvodů. Důležitý je nejen jazyk samotný, ale také jeho vhodnost pro řešení konkrétního problému, množství dostupných nástrojů a počet kvalitních vývojářů. Není příliš obvyklé, aby měl běžný programátor zkušenosti s formálními metodami. V případě programátorů v jazyce Haskell je tato četnost vyšší. Navíc je neobvyklé najít zkušené vývojáře Haskellu bez detailních znalostí informatiky.

V souvislosti s potřebou používat formální metody pro vývoj Cardana byl Haskell jednou z přirozených voleb. Cardano je budováno jako kritický projekt a Haskell má ve své DNA vlastnosti, které pomáhají tohoto cíle dosáhnout.

Článek připravili Cardanians s podporou Cexplorer.

Přečtěte si celý článek: https://cexplorer.io/article/why-did-iog-choose-haskell-to-build-cardano