Ale kompilátor může vědět něco o symbolické matematice a nějaké další matematické axiomy ho můžeme naučit.
Ano, některé věci můžeme schovat do knihoven a knihovny klidně do kompilátoru nebo až do procesoru. Ty pak bereme za dané a podle míry jejich složitosti už je ani netestujeme. Programátoři dnes obvykle neprogramují, jak sečíst dvě 32bitová čísla, ale spoléhají na to, že to instrukce procesoru děla správně. Pořád je ale potřeba programátor na to, aby procesoru „vysvětlil“, že když má v jednom registru částku a v druhém registru DPH, cenu s DPH spočítá právě sečtením těch dvou registrů.
A systémy, které umí symbolickou matematiku tady máme a když se jich zeptáme, jestli daný vzoreček řeší kvadratickou rovnici, tak jsou schopny na to dát jasnou odpověď. Ne vždycky (halting problem), ale o to nejde.
Ano, ale k tomu musíme umět tou symbolickou matematikou popsat, co je to kvadratická rovnice. A pokud tomu systému popíšu kvadratickou rovnici jako součet násobku druhé mocniny proměnné a násobku proměnné, tj. zapomenu na to, že v kvadratické rovnici může být také konstanta, ten systém to nijak nezjistí. V systému symbolické matematiky je taková rovnice možná, je to podmnožina kvadratických rovnic. A není to chyba toho systému ani odvozování, je to chyba v převodu mezi reálným světem a formálním jazykem (v tomto případě symbolickou matematikou).
Konec konců, ten příklad s leftPad je moc hezký - copak typový systém ví něco o zarovnávání z leva? Ale dá se mu to vysvětlit.
Ano, naprogramovat se dá leccos, i mnohem složitější věci, než je zarovnávání zleva :-) A jsou různé způsoby, jak to naprogramovat, dá se to naprogramovat imperativně i deklarativně a
je to vzájemně převoditelné. Rozdíl není na straně počítače (i když fakticky se nakonec vše převádí na imperativní, protože tak pracují dnešní procesory), rozdíl je na straně lidí – některé věci se nám lépe vyjadřují deklarativně, některé raději vyjadřujeme imperativně.
Ale myslím, že je trošku nepochopení, k čemu typový systém je.
Taky si myslím. Typový systém je jen jiný způsob vyjádření, nic míň, ale ani nic víc.
Jenomže to jde otestovat leda tak, že se napíše specifikace, která bude vypadat přesně stejně. Takže se problém chyby přesune od kódu ke specifikaci a vůbec nic to nevyřeší, jen místo toho, zda kód je správně budeme řešit, jestli specifikace je správně.
Ano, to tvrdím od začátku. Takhle se to ale dá odsouvat do nekonečna, a o správnosti se nedozvíme nikdy nic. Proto se často testuje to, že vezmu něco mnohem jednoduššího, než specifikaci, o čem ale vím, že je to správně, a otestuju jenom tyhle zaručeně správné případy. Tím nezískám odpověď na otázku, zda je to celé správně, ale dozvím se alespoň to, že tam je aspoň něco správně.
IMO typový systém (nebo obecně dokazování) má smysl tam, kde specifikace a kód není totéž. Ale jinak bych zopakoval, že u všech těchto věcí (testy, typy) je vhodné si položit otázku, zda se to vyplatí - a při dobrém využití typů (na doméně, kde to funguje dobře) výhoda těch testů dost klesá, protože těch chyb je tam z principu výrazně méně.
A stejně tak existují domény, kde nesou potřeba žádné složité typy a kde zároveň největší množství chyb vzniká při převodu mezi neformálním zadáním a formálním programovacím jazykem. A tam je zase minimum chyb, které by bylo možné odstranit lepšími typy.
Zobrazit příspěvky
? Vůbec nerozumím. Celý tenhle thread je o tom, že mám k dispozici kompilátor, který "něco"(typy) umí, a zda s pomocí toho "něčeho" jsem schopen nějaký další program verifikovat tak, že unit testy potřebovat nebudu. Takže když píšu, že pokud bychom měli kompilátor schopný řešit matematické výrazy, tak to umí i verifikovat řešení kvadratické rovnice. Vůbec nechápu, co s tím má společného,
