Knižní recenze: Göedel's Proof (diskuse)

[Xerces]

Díky za pěknou upoutávku.

[mirefek]

Jo, tohle jsem si kdysi taky rozmýšlel, a coby počáteční impuls mi stačil čistě jenom Halting Problem, je to vlastně dost analogické tvrzení, a možná se o tom ani tak moc neví (knížku neznám, ale zdejší ajťáky by to mohlo zajímat).

Halting Problem říká, že neexistuje algoritmus, který dostane na vstupu algoritmus, a v konečném čase odpoví, jestli algoritmus skončí, nebo ne. Dokazuje se to tak, že se za pomocí takového oracula sestaví algoritmus se sporným chováním -- jistou chytrou sebereferencí (tu teď nevysvětluji podrobně, mohl bych, pokud by byl zájem) se sestrojí algoritmus, který skončí právě tehdy, když o sobě rozhodne, že neskončí.

A Gödelova věta se pak dá ukázat skoro stejně -- stejným sebereferenčním trikem se sestaví algoritmus, který dělá pouze to, že se snaží najít matematický důkaz, že se on sám nezastaví. A až ho najde, tak se spokojeně ukončí. V opačném případě prostě hledá a hledá napořád. (docela přirozené chování, řekl bych) Tak přesně vznikne výrok V (že se náš algoritmus zastaví), který je ekvivalentní výroku "dá se dokázat negace V".

A po chvilce hraní je možné ukázat ekvivalenci výroku V s tím, že "formálně lze dokázat spor z ničeho", čímž se dostane slavný výsledek "Matematika je bezesporná právě tehdy, když to o sobě neumí dokázat."

[Bystroushaak]

Halting Problem říká, že neexistuje algoritmus, který dostane na vstupu algoritmus, a v konečném čase odpoví, jestli algoritmus skončí, nebo ne. Dokazuje se to tak, že se za pomocí takového oracula sestaví algoritmus se sporným chováním -- jistou chytrou sebereferencí (tu teď nevysvětluji podrobně, mohl bych, pokud by byl zájem) se sestrojí algoritmus, který skončí právě tehdy, když o sobě rozhodne, že neskončí.

Jo, je to podobné, ale Göedel jde imho dál, protože rozšlapal bábovičky obecně axiomatickým systémům (kterým je imho i Turingův stroj), ale naopak to afaik neplatí.

[mirefek]

To jo, Gödelova práce má rozhodně dalekosáhlejší filosofické důsledky.

Jenom mi přišlo, že "ten trik" v důkazu je možnost sebereference tam, kde by člověk doufal, že to nepůjde. Jako je jasné, že věta "Tahle věta je nepravdivá" je taková nesmyslná, takže se naštěstí pomocí formálního jazyka nedá ani vyslovit. Proto člověka zarazí, že věta "Dá se dokázat negace téhle věty." vedoucí ke skoro stejným paradoxům už ve formálním jazyce dostat lze. A obzvlášť programátorovi bych to uvedl přes cvičení "Zkuste napsat program, který vypíše svůj zdrojový kód".

A nemyslím si, že Gödel nějak zásadně "rozšlapal bábovičky", Russelův paradox byl imho pro matematiku o dost větší přůšvih. Gödel spíš akorát poukázal na to, že to jsou opravdu jenom "bábovičky" -- zbořil naivní představy, které nebyly ve skutečnosti ničím podložené. podobně jako byla ve starověku představa, že všechna čísla jsou racionální. Ale je to velký rámus, když padají ideály

[Abraxis]

https://en.wikipedia.org/wiki/Quine_(computing) :)

[mirefek]

Díky, dobrý vědět, jak se to jmenuje.

[Ondrej Santiago Zajicek]

Jako je jasné, že věta "Tahle věta je nepravdivá" je taková nesmyslná, takže se naštěstí pomocí formálního jazyka nedá ani vyslovit.

Ona se neda vyslovit primarne proto, ze formalni jazyk se nezabyva pravdivosti, ale dokazatelnosti.

Proto člověka zarazí, že věta "Dá se dokázat negace téhle věty." vedoucí ke skoro stejným paradoxům už ve formálním jazyce dostat lze.

Problem je v tom, ze 'da se dokazat' neznamena presne to same na metaurovni logiky prvniho radu a pri reformulaci jazykem aritmetiky uvnitr logiky prvniho radu.

A nemyslím si, že Gödel nějak zásadně "rozšlapal bábovičky", Russelův paradox byl imho pro matematiku o dost větší přůšvih.

On to je obecny vyvoj matematiky smerem k vyssi preciznosti - nejdrive se prijde s nejakym intuitivnimi pristupem, pak se ukaze, ze pri neopatrne praci se clovek poreze, a nasledne se zavede preciznejsi formalizace. Napr. nekonecne mala cisla v analyze a epsilon-delta notace, ci naivni teorie mnozin s paradoxy a axiomatizovana teorie mnozin. Godelova prace ukazuje, ze si clovek musi davat pozor pri rozlisovani jednotlivych metarovin. Skolemuv paradox ukazuje, ze ani kardinalita neni absolutni meritko.

[aaa]

Jako je jasné, že věta "Tahle věta je nepravdivá" je taková nesmyslná, takže se naštěstí pomocí formálního jazyka nedá ani vyslovit.

Ona se neda vyslovit primarne proto, ze formalni jazyk se nezabyva pravdivosti, ale dokazatelnosti.

Preco nie? Je to iba viac na strane semantiky. V modeli formule platia, v teorii sa hovori o dokazatelnosti. Ked je formula dokazatelna, tak je plati v kazdom modeli. Obratena implikacia plati vo vyrokovej logike.

[Jendа]

Jo, tohle jsem si kdysi taky rozmýšlel, a coby počáteční impuls mi stačil čistě jenom Halting Problem

Osobně jsem měl na složitosti asi největší WOW z věty, že busy beaver funkce je nevyčíslitelná. Gödelovy věty byly bohužel až na úplně poslední přednášce a nestihly se tak moc probrat (ale jinak Gregor přednášel pěkně).

[Ondrej Santiago Zajicek]

Göedel tím dokázal, že axiomatické systémy nemůžou být použity k „vytěžení“ celé matematiky iterací přes platné axiomatické výrazy, protože axiomatické systémy obsahují jednak paradoxy, které jsou nerozhodnutelné, ale také jakési ostrovy platných vět, ke kterým se není možné dostat odvozováním z axiomatických systémů.

Tady bych byl opatrnejsi. Predstava, ze je 'jedna matematika', kterou postupne objevujeme, a axiomy jsou nejake zjevene pravdy o ni, vzala za sve uz s Lobacevskym. Na matematiku lze pohlizet jako na prostor moznych struktur, ktery pomoci axiomu uchopujeme - vymezujeme si jimi ty struktury, ktere nas zajimaji (a podle toho jsme zvolili axiomy). Axiomaticky system je pak stale mozne pouzit 'k vytezeni' vsech pravdivych ci nepravdivych tvrzeni a dane tride struktur vymezene temi axiomy (to rika Godelova veta o uplnosti), ale jazyk predikatove logiky prvniho radu neni casto dostatecne precizni, abych jim byl schopen presne vymezit ty struktury, ktere me zajimaji (napr 'standardni prirozena cisla') od tech struktur, ktere uz me nezajimaji (napr. prirozena cisla rozsirena o nestandardni prvky).

Nelze tedy mluvit (v predikatove logice prvniho radu) o 'ostrovech platnych vet, ke kterym se neni mozne dostat odvozovanim'. Pokud se k takove vete nelze dostat dokazovanim, pak neni platna (ve smyslu pravdivosti vety v teorii), nebot v nektere strukture popsane danou teorii ta veta neni pravdiva, prestoze v te strukture, ktera nas zajima, pravdiva je. Jina situace je v jinych formalnich systemech nez predikatova logika prvniho radu, kde nemusi platit Godelova veta o uplnosti. Tam mohou byt 'plne' pravdiva ale nedokazatelna tvrzeni.

Tady bych jeste zminil mene proflaklou ale nemene zajimavou Lowenheim-Skolemovu vetu, ktera rika, ze i kdyz uz tu tridu struktur popisuji dostatecne presne (pomoci treba nerekurzivni ale spocetne sady axiomu) tak, ze vsechna tvrzeni jsou bud dokazatelna nebo vyvratitelna, stejne ty struktury mohou byt neizomorfni kvuli odlisne kardinalite.

Göedelův důkaz má poměrně velké důsledky také pro sféru computer science, neboť ukazuje, že statická analýza je ze své podstaty nekompletní.

Ty dopady mimo oblast matematiky a logiky bych zas tak vyznamne nevidel. Ve staticke analyze nepotrebuji vytvorit uplny system, ale staci mi najit takove (bezesporne) axiomy, ktere jsou dostatecne k dokazani tech tvrzeni, ktere me o kodu zajimaji. V praxi potom systemy na statickou analyzu kodu budou stejne pouzivat slabsi inferencni mechanismy, nebot mezi 'analyza dobehne za 200 let' a 'analyza nedobehne' uz zas takovy rozdil neni.

[Bystroushaak]

Zajmavé.

[Sten]

Malá jazyková: Gödel nebo Goedel, ale ne Göedel

[Bystroushaak]

Hah, díky.

[Bystroushaak]

Hrozný brain damage tohle. Jakože doslova jsem to nebyl schopný vidět.

[Petr]

Já četl toto https://www.levneucebnice.cz/p/neuplnost-dukaz-a-paradox-kurta-godela/, taky se mi to líbilo, je tam i něco o životě K.G., o jeho vztahu k Einsteinovi apod.

Už je to nějaký pátek, co jsem to četl, ale já si to zapamatoval cca tak, že on dokázal, že každý systém který obsahuje aritmetiku, musí obsahovat i výroky, o nichž víme, že jsou pravdivé, ale nemůžeme je dokázat. Tím rozšlapal bábovičky všem hnutím formalistů, ti již měli mezi matematickými problémy pro 20.století něco jako "dokázat aritmetiku v rámci sama sebe". Dále jako vedlejší produkt dal naději, že člověk nemůže být jen velmi složitý stroj.

[Ivorne]

Tyhle teorie o logických paradoxech jsou tak trochu nesmysl. Je potřeba si dát velký pozor, jak se interpretují a mám pocit, že i velké množství lidí, kteří se jimi teoreticky zabývají (asi včetně Goedela), to často dělají nesprávně. Ty paradoxy nejsou ve skutečnosti v daném axiomatickém systému, ale jsou následkem nekorektního použití těchto axiomatických systémů.

Je to jako ty výpočty, co se občas objevují na facebooku a podobně, kde na začátku máme jednoduchou rovnici 1=1 a po sekvenci zdánlivě korektních operací vznikne nesmysl jako třeba 1=5 (příklad: https://skullsinthestars.files.wordpress.com/2008/12/neg1equals1.png?w=640). Problém je vždycky v tom, že je tam jeden nekorektní krok, který se jenom těžko odhaluje. Typicky to bývá dělení obou stran rovnice nulou nebo umocňování obou stran rovnice, což je korektní jen za určitých podmínek. Stejně tak je to s těmi logickými paradoxy, ale tam tou nekorektní operací bývá referencování budoucnosti nebo sama sebe.

Podle toho, co píšeš v blogu, si Goedel byl vědom rizika použití nekorektních operací: "Kódování do čísel bylo důležité, aby se vyhnul chybám, které dělají lidé předpokládáním nějakého chování.". Ale podle mě se mu stejně nepovedlo se tomu vyhnout. On sice zakóduje tvrzení do čísla, ale pak to vypadá, že s ním operuje zase pouze slovně a ne pomocí kódování. Protože kdyby se ten teorém "Konkrétní přirozené číslo ‚g‘ není dokazatelné číslo." pokusil zakódovat sám se sebou na vstupu, tak by se mu to nepovedlo, protože by neznal vstup (zakódovaný teorém) dokud by nedokončil kódování, což by zase nemohl udělat, když by ještě neznal celý vstup do toho kódování. Zkrátka řečeno - selže už jen snaha zakódovat ten teorém do čísla a k verifikaci toho teorému se vůbec nedostaneme. Čili ten teorém není součástí množiny teorémů popsatelných tím axiomatickým systémem. Čili to není paradox. To by bylo jako napsat kód v Javě a pak se divit, že ho nejde spustit pomocí interpreteru Pythonu.

Napadl mě jednoduchý logický paradox, který ukazuje, jak jsou tyhle paradoxy nesmyslný koncept. Tvrzení je: "Pokud tvrdíš, že toto tvrzení je lež, pak říkám, že tráva je zelená. Pokud ale tvrdíš, že toto tvrzení je pravda, pak říkám, že tráva je současně čistě modrá i čistě červená.". Toto tvrzení je 'paradox', ale ne proto, že by byla nějaká vada v axiomatickém systému, ale proto, že ten text ve skutečnosti neobsahuje celé tvrzení. Nelze definitivně rozhodnout, co to tvrzení vlastně říká, protože je záměrně postaveno tak, že určitá jeho část bude vždy mimo dosah koholiv, kdo se pokusí ho verifikovat. A když nemám během verifikace k dispozici celé tvrzení, které se snažím verifikovat (a ani nemohu mít), tak ho těžko mohu verifikovat. Je to jako pokusit se verifikovat tvrzení "A==1" za situace, kdy neznám A a selhání pak svádět na chybu operace porovnání.

Poučení, které by si měl člověk vzít z těchto teorií o logických paradoxech je, že lze snadno vytvořit tvrzení, které vypadá jako že vzniklo opakovanou validní aplkací základních axiomů axiomatického systému, ale ve skutečnosti tak vzniknout nemohlo. Exituje už i nějaká teorie o tom, jak se těmto 'paradoxům' vyhnout. Zkráceně řečeno stačí udělat tvrzení tak, že poposuje pouze věci z nižších logických metarovin (~věci v minulosti) a nepopisuje tedy nic ze svojí metaroviny (~věci v přítomnosti) nebo z vyšší metaroviny (~věci z budoucnosti). Bohužel k tomu nemůžu dlouhodobě najít žádné zdroje, takže jestli máte někdo odkaz, tak bych ho ocenil.

Myslím, že se ty metaroviný dají aplikovat i tak, že řekneme, že tvrzení "Toto tvrzení je lež" je pravdivé v každé druhé metarovině a v těch ostatních je nepravdivé (je to prostě na střídačku vždycky pravda a lež). Prostě řekneme, že tvrzení označované výrazem 'toto tvrzení' ve skutečnosti označuje stejně formulované tvrzení v o jedna nižší metarovině a verifikace potom rozhoduje o tom, ve kterých všech metarovinách je tvrzení pravdivé a ve kterých ne.

[Ondrej Santiago Zajicek]

Tyhle teorie o logických paradoxech jsou tak trochu nesmysl. Je potřeba si dát velký pozor, jak se interpretují a mám pocit, že i velké množství lidí, kteří se jimi teoreticky zabývají (asi včetně Goedela), to často dělají nesprávně. Ty paradoxy nejsou ve skutečnosti v daném axiomatickém systému, ale jsou následkem nekorektního použití těchto axiomatických systémů.

To je castecne pravda pro ruzne 'verbalni' paradoxy a pro ruznou snahu vysvetlit ty paradoxy laikum pomoci prosteho textu (ktery byva nedostatecne precizni pro tyto ucely) a pripadne pro uvahy o ruznych 'filosofickych presazich' tech paradoxu, nicmene existuji korektni logicke a matematicke paradoxy a ty odmitnout nejde.

V podstate jde o dva typy paradoxu: 'Prave' paradoxy, antimonie, ktere ukazuji na zasadni chybu v teorii nebo v metode inference (napr. znamy Russelluv paradox a Kleene–Rosseruv paradox), a pak 'neprave' paradoxy, paradoxni stav veci, kde je teorie, logika i odvozeni v poradku, ale (spravny) vysledek je ve vyraznem rozporu s nasim intuitivnim chapanim a casto vede k presnejsi konceptualizaci dane problematiky. To je priklad treba Banach-Tarskeho paradoxu ci Skolemova paradoxu, nebo prave Godelovych vet.

[Bystroushaak]

Podle toho, co píšeš v blogu, si Goedel byl vědom rizika použití nekorektních operací: "Kódování do čísel bylo důležité, aby se vyhnul chybám, které dělají lidé předpokládáním nějakého chování.". Ale podle mě se mu stejně nepovedlo se tomu vyhnout. On sice zakóduje tvrzení do čísla, ale pak to vypadá, že s ním operuje zase pouze slovně a ne pomocí kódování. Protože kdyby se ten teorém "Konkrétní přirozené číslo ‚g‘ není dokazatelné číslo." pokusil zakódovat sám se sebou na vstupu, tak by se mu to nepovedlo, protože by neznal vstup (zakódovaný teorém) dokud by nedokončil kódování, což by zase nemohl udělat, když by ještě neznal celý vstup do toho kódování. Zkrátka řečeno - selže už jen snaha zakódovat ten teorém do čísla a k verifikaci toho teorému se vůbec nedostaneme. Čili ten teorém není součástí množiny teorémů popsatelných tím axiomatickým systémem. Čili to není paradox. To by bylo jako napsat kód v Javě a pak se divit, že ho nejde spustit pomocí interpreteru Pythonu.

Tady děláš klasickou internetovou chybu, a to je že se snažíš odvodit smysluplnost či pravdivost na základě popisu, místo věci samotné. Celé jsem to samozřejmě tisíckrát zjednodušil, samotný důkaz je podstatně rigoróznější, než to co jsem napsal já. Fakt doporučuji si tu knížku přečíst, nebo přímo důkaz samotný. Ostatně, Gödel o tom přesvědčoval matematiky, včetně samotných tvůrců Principie Mathematiky, tak je ten jeh důkaz na jiné úrovni. Já jsem v matematice jen laik.

[Ivorne]

Jsem tušil, že mi tohle vytkneš. Ale na mojí pointě to nic nemění. Vyznám se spíš v halting problému. O tomhle zobecnění na všechny výpočetní modely jsem ale taky už dřív slyšel a nevidím v pointě těch důkazů velký rozdíl.

Vem si třeba právě ten halting problém. Tam se v podstatě říká, že existuje aspoň jeden program u něhož nelze určit, zda skončí nebo ne. Důkaz toho tvrzení spočívá v tom, že se popíše ten neurčitý program. Ale vem si, že ten program se nedá reálně sestrojit. To, že existuje nějaký popis toho programu přece neznamená, že ten program existuje nebo že jde napsat. Ten popis toho programu pouze působí dojmem, že se dá vyrobit malou úpravou jiného existujícího programu (programu, který určí, zda program na vstupu někdy skončí). Ale reálně se sestrojit nedá. Ta malá úprava ve skutečnosti do celého procesu sestavení toho programu zavádí nutnost znát budoucnost (nutnost znát podobu programu ještě dřív než ho sestavíš). Takže se ve skutečně nejedná o zas tak malou úpravu.

Takže sice nejde napsat program, který pro každý program na vstupu určí, zda ten program skončí nebo ne. Ale jde napsat program, který pro každý napsatelný program určí, zda skončí, nebo ne. A protože množina nenapsatelných programů, o kterých by tě zajímalo, zda skončí nebo ne, je nejspíš prázdná, tak je důkaz neurčitosti halting problému celkem k ničemu.

[Bystroushaak]

O tomhle zobecnění na všechny výpočetní modely jsem ale taky už dřív slyšel a nevidím v pointě těch důkazů velký rozdíl.

Jo, já o tom taky slyšel, jenže co tak chápu, tak to co jsi napsal stejně není řešení všech paradoxů. Spíš mi šlo o to, abys moc nespoléhal na to co jsem psal, protože jak to funguje vím asi měsíc a nikdy dřív jsem to nestudoval.

Vem si třeba právě ten halting problém. Tam se v podstatě říká, že existuje aspoň jeden program u něhož nelze určit, zda skončí nebo ne. Důkaz toho tvrzení spočívá v tom, že se popíše ten neurčitý program. Ale vem si, že ten program se nedá reálně sestrojit. Ale vem si, že ten program se nedá reálně sestrojit. To, že existuje nějaký popis toho programu přece neznamená, že ten program existuje nebo že jde napsat.

Proč by se nedal reálně sestrojit? V tomhle tvůj argument úplně nechápu.

[mirefek]

Takže sice nejde napsat program, který pro každý program na vstupu určí, zda ten program skončí nebo ne. Ale jde napsat program, který pro každý napsatelný program určí, zda skončí, nebo ne. A protože množina nenapsatelných programů, o kterých by tě zajímalo, zda skončí nebo ne, je nejspíš prázdná, tak je důkaz neurčitosti halting problému celkem k ničemu.

To teda těžko, leda že by ten program, co "jde napsat", byl nenapsatelný

Jinak by mě zajímalo spousta programů, jestli skončí, nebo ne. Třeba takový program, který hledá sudé číslo větší než dva, které se nedá rozložit na součet dvou prvočísel, a skončí, až ho najde.

[mirefek]

Tady je když tak kód toho programu, který mě zajímá, napsaný v Pythonu, abych demonstroval, že je napsatelný. Netvrdím, že se jedná o nerozhodnutelný problém (kdybych to věděl, tak bych musel mimo jiné vědět, že ten program neskončí, což se u nerozhodnutelných problémů dělá těžko). Ale dost pochybuji, že by takový kód šel předložit nějakému existujícímu automatu, a ten mi dal odpověď. Nejnadějnější by mohly být dokazovací automaty (když nebude vadit mrtě velký výpočetní čas), ale jak je patrné právě z Gödelovy věty, ani ty nejsou dokonalé.

def is_prime(n):
    if n < 2: return False
    for d in range(2, n):
        if n%d == 0: return False
    return True

def is_decomposable(n):
    for n1 in range(1, n):
        n2 = n - n1
        if is_prime(n1) and is_prime(n2):
            print("{} = {}+{}".format(n, n1, n2))
            return True
    return False

n = 4
while is_decomposable(n): n += 2
print("{} is not decomposable".format(n))

[Jendа]

Ale jde napsat program, který pro každý napsatelný program určí, zda skončí, nebo ne.

Ale když máš takový program, volání podprogramů a podmíněný skok (což jsou IMHO featury, bez kterých by tvůj výpočetní model byl nepoužitelně slabý), tak můžeš sestrojit přesně ten program, o kterém jsi před chvílí napsal, že reálně sestrojit nejde:

def trolling(program):
  if willHalt(program, program):
    while True:
      pass

(což je napsatelný program, protože jsem ho právě napsal :), a o programu volajícím trolling(trolling) nelze říct, jestli se zastaví, nebo ne)

[zvol]

Tam se v podstatě říká, že existuje aspoň jeden program u něhož nelze určit, zda skončí nebo ne.

To se tam ale právě neříká.

[deda.jabko]

A protože množina nenapsatelných programů, o kterých by tě zajímalo, zda skončí nebo ne, je nejspíš prázdná

To je prave chybny predpoklad. Testovat programy, o kterych vis, ze skonci, by bylo asi stejne prinosne, jako divat se na fotbalovy zapas, o kterem vis, jak dopadne.

Nechci rozjizdet dalsi flame, ale halting problem mi prijde takovy precenovany. Je to proste takove to popularni tema, ke kteremu se da jednoduse vyjadrovat i po patem pivu. Pricemz ve vycislitelnosti jsou podle me mnohem hezci a praktictejsich veci. Napada me treba kombinator pevneho bodu v lambda kalkulu, churchovo kodovani cisel, a kdyz jsme u toho i nerozhodnutelnost, zda jsou dva lambda vyrazy ekvivalentni. Cimz se obratem dostavame k problemum typu zastaveni, pricemz tato formulace muze vypadat uzitecneji, nez problem zastaveni.

[NaN]

Liško Bystrouško, zmizela ti adresa etherea. Proč ? Já bych spíš čekal, vzhledem k událostem, že ti zmizí adresa bitcoinu.

[Bystroushaak]

Dal jsem jí pryč protože tam nikdy nikdo nic neposlal. A taky protože jsem zapomněl heslo, a šestihodinový BruteForce složený z mých běžný hesel nepomohl :S Ještě štěstí že tam nic nebylo.

[NaN]

Chápu, investoval jsi ale přece do etherea ne ? Jak vidíš jeho budoucnost ? Respektive jaký máš celkově názor na vývoj technologie blockchainu? Jaký bude podle tebe svět za 10 let ?

[Bystroushaak]

Investoval jsem do všeho možného, ne jenom Etherea. Momentálně jsem investoval například do Sia coinu a Dao (do obojího ale jen pár tisíc). Z Etherea jsem měl vyšší desítky tisíc, ale prodal jsem ho moc brzo. Kdybych s tím počkal půl roku tak jsem si za to mohl koupit například byt. Tohle je obecně problém krypto-měn, že nikdy nevíš jestli už je to na vrcholu, nebo to bude dál stoupat. Zrovna Ether v té době padl na docela málo, a čtvrt půl roku byl relativně nízko, a mě už fakt nebavilo to sledovat a řešit, tak jsem se ho zbavil.

Blokchain má samozřejmě budoucnost, včetně etherea. Myslím že Ethereum je momentálně ze všeho nejperspektivnější co do technologie, myšlenky, provedení a skupiny lidí, co za ním stojí. Pomalu se ale vynořují i další krypto-měny založené na myšlenkách podobných chytrým kontraktům. Například ten Sia. Podle mě se brzké době objeví hodně různých vyrovnávacích měn, které budou nabízet výměnu například výpočetního výkonu za coin, který později můžeš vyměnit zpět za výpočetní výkon, nebo třeba za úložný prostor, nebo louskání captchi. To je docela praktická věc, proto si myslím, že jich bude všude kopec. Peníze podložené reálnou věcí, jako je třeba gigabajt prostoru na hodinu, které získáš když nabídneš gigabajt prostoru na hodinu, a můžeš si vyzvednout, když nabídneš patřičný coin. Stará dobrá směnná jednotka, asi jako když byly dřív peníze podložené zlatem a fakt jsi mohl přijít do banky a nechat si za ně vyplatit to zlato. Taky to bude mít výhodu, že nebudeš zbytečně pálit výkon, jako v případě bitcoinu.

Myslím že Ethereum bude dlouhodobě sloužit jako technická platforma pro realizaci, a to i v daleké budoucnosti, i když samotné zas tak zajímavé není a vzniknou zajímavější nápady a realizace. Jedna z těch původních myšlenek totiž byla, aby se na tom daly stavět různé další nápady, bez toho abys musel řešit všechny možné technické detaily, jako je například navazování spojení v P2P sítí, nebo ověřování jednotlivých klientů. Z Etherea se tak může časem stát něco podobného, jako TCP/IP; takový základní podkladový protokol pro stavbu zajímavějších uživatelských nápadů.

Já už celou tu scénu zas tak moc nesleduju, což je nejspíš moje vlastní škoda. Jenže to žere tak moc času, že mě to nebaví. Dostal jsem se ale omylem do docela divné pozice, kde platím za experta na krypto-měny, takže mi píšou lidi na email s různými doporučeními, nebo žádostmi o radu. Například jsem takhle radil nějaké ženské co má napsat do bakalářky. Taky mě překvapilo kolik lidí mě referencuje v různých pracích, když jsem si hodil URL do google. Přitom to není tak že bych měl nějaké extra znalosti, všechno co vím si může načíst každý během pár týdnu čtení.

Moje představa budoucnosti je trochu rozebraná v blogu Vytváření prostorů otevíráním dimenzí. Specificky v té koncové části. Ethereum má podle mě slušnou šanci se stát podkladovou jednoticí platformou pro IoT. Mluvil jsem o tom s několika různými lidmi, například s Vladem Kahounem z broadapi, nebo na pohovoru s Nordic Telecomem, kde se tvářili, jako že je to fakt hodně zajíma, a že by na tom chtěli stavět produkty.

Sám nad tím momentálně nic nestavím, protože nemám čas. Práce mi žere většinu produktivního času. Ten zbytek věnuju programování věcí, které jsou pro mě momentálně zajímavější, a psaní (ať už blogů, nebo knížky, nebo věcí které jsem zatím nepublikoval a publikovat nehodlám). Rád bych dneska publikoval blog s detaily.

Mimochodem tenhle příspěvek byl z velké části nadiktována na iPhonu, v rámci experimentování s různými divnými uživatelským rozhraními.