Dědičnost dnes

[balki]

Jediné dynamické jsou data z venku. Což ale právě ten můj systém nemůže rozbít, protože vše je jasně definované.

Nebo mi něco uniká?

Uniká ti tohle: https://en.wikipedia.org/wiki/Halting_problem

A jak to souvisí s reálným světem reálného OOP v Javě? Nechci nic za chodu měnit! Víš, kolik jsem viděl lopat, které debugovaly kód, který se jim měnil? Při každém průchodu tam měly něco jiného, protože byly cool a dynamické věci jsou přece víc agilní.

Rád ti to vysvětlím. Už v roce 1936 Alan Turing dokázal, že nexistuje obecný algoritmus, který by řešil problém zastavení pro všechny vstupy všech programů na Turingově stroji. Možná víš, že Java je Turing complete programovací jazyk. Prakticky to znamená, že nelze rozhodnout jestli je nějaký (netriviální) program (v Javě) správný a bude fungovat pro jakýkoliv vstup. Tvoje tvzení:

Jediné dynamické jsou data z venku. Což ale právě ten můj systém nemůže rozbít

je nesmysl, který tvrdíš, protože neznáš základy IT.

Přehlédl jsi v tom Alanově vyjádření to "obecný algoritmus".

A tiez v praxi sa nedokazuje, ci je algoritmus formalne spravny, ale ci sa chova spravne pre urcite vstupy a vystupy.
Formalne dokazovanie sa robi tak v NASA? Mozno ani tam nie?

[Reklama]

[lopata]

Přehlédl jsi v tom Alanově vyjádření to "obecný algoritmus".

Ne nepřehlédl a nahradil jsem ho slovem netriviální, protože prakticky to platí. Pro netriviální programy je to prakticky neřešitelné.

[lopata]

A tiez v praxi sa nedokazuje, ci je algoritmus formalne spravny, ale ci sa chova spravne pre urcite vstupy a vystupy.
Formalne dokazovanie sa robi tak v NASA? Mozno ani tam nie?

Pro určité vstupy to dokázat lze. Pro libovolný vstup to pro (netriviální) programy dokázat nelze.

[lopata]

hledejte "formal verification"
taky "znát" vs. "rozumět"

Formálně ověřit lze jen určité typy programů. Kdybys uměl formálně ověřit jakýkoliv program, vyřešil bys halting problem. Asi bys za to dostal Nobelovku.

[BoneFlute]

A tiez v praxi sa nedokazuje, ci je algoritmus formalne spravny, ale ci sa chova spravne pre urcite vstupy a vystupy.
Formalne dokazovanie sa robi tak v NASA? Mozno ani tam nie?

Pro určité vstupy to dokázat lze. Pro libovolný vstup to pro (netriviální) programy dokázat nelze.

No, a proto nepíšu obecné algoritmy pro libovolný vstup, ale konkrétní algoritmy pro konkrétní množinu dat.

Čímž se dostáváme zpět k tomu, že statickým typováním si určuju tu množinu, že jo.

[Reklama]

[v]

hledejte "formal verification"
taky "znát" vs. "rozumět"

Formálně ověřit lze jen určité typy programů. Kdybys uměl formálně ověřit jakýkoliv program, vyřešil bys halting problem. Asi bys za to dostal Nobelovku.

naštěstí praktický význam mají jen určité typy programů
a možná jste měl na mysli spíš Fieldsovu medaili

[lopata]

No, a proto nepíšu obecné algoritmy pro libovolný vstup, ale konkrétní algoritmy pro konkrétní množinu dat.

Čímž se dostáváme zpět k tomu, že statickým typováním si určuju tu množinu, že jo.

Množinu zúžíš, ale to je hodně daleko od vyřešení halting problému pro konkrétní program. On může být velice triviální:

Kód: [Vybrat]

def collatz_sequence(x):
    seq = [x]
    while x > 1:
       if x % 2 == 0:
         x = x / 2
       else:
         x = 3 * x + 1 
       seq.append(x)
    return seq

Dokaž, že to skončí pro jakékoliv x. Ušetřím ti práci, formálně to ještě nikdo nedokázal.

[lopata]

naštěstí praktický význam mají jen určité typy programů
a možná jste měl na mysli spíš Fieldsovu medaili

Prakticky každý netriviální program je nerozhodnutelný. Viz např. Collatz conjecture.

[javaman ()]

naštěstí praktický význam mají jen určité typy programů
a možná jste měl na mysli spíš Fieldsovu medaili

Prakticky každý netriviální program je nerozhodnutelný. Viz např. Collatz conjecture.

Pořád to ale nikoho v praxi nezajímá. Nevím, co tu řešíš. Jestli se učíš do školy, tak v pohodě, ale jinak jsou to nesmysly někoho, kdo nikdy nic reálného nedělal.

Aha, takže jsi línej si to přečíst a porozumět tomu, tak křičíš že to jsou kecy. Tady končím s diskuzí.

Kdybych měl číst každý žvást na netu, tak nedělám nic jiného. Ten tvůj test je bez kódu také úplně k ničemu.

jsem blbec, predtim jsem to omylem smazal, tady to je https://gist.github.com/anonymous/af62e39e832bafc77122c2bb08d76d58

OK, dík.

[lopata]

Pořád to ale nikoho v praxi nezajímá. Nevím, co tu řešíš. Jestli se učíš do školy, tak v pohodě, ale jinak jsou to nesmysly někoho, kdo nikdy nic reálného nedělal

Tebe to nezajímá, ty si prostě řekneš, já jsem guru, můj program bude fungovat pro jakýkoliv vstup a za to se zaručím. Tak tvoje volba. Ve své omezenosti bohužel nevidíš, jak moc jsi hloupý a nezkušený.

[v]

naštěstí praktický význam mají jen určité typy programů
a možná jste měl na mysli spíš Fieldsovu medaili

Prakticky každý netriviální program je nerozhodnutelný. Viz např. Collatz conjecture.

možná jsem přízemní, ale k čemu to je dobré? znamené to že nejde ověřit (řekněme že skončí a že mu nepřetečou celočíselné proměnné) program na hlídání provozních parametrů turbíny?

[javaman ()]

naštěstí praktický význam mají jen určité typy programů
a možná jste měl na mysli spíš Fieldsovu medaili

Prakticky každý netriviální program je nerozhodnutelný. Viz např. Collatz conjecture.

možná jsem přízemní, ale k čemu to je dobré? znamené to že nejde ověřit (řekněme že skončí a že mu nepřetečou celočíselné proměnné) program na hlídání provozních parametrů turbíny?

+1

[lopata]

možná jsem přízemní, ale k čemu to je dobré? znamené to že nejde ověřit (řekněme že skončí a že mu nepřetečou celočíselné proměnné) program na hlídání provozních parametrů turbíny?

Nelze ani ověřit, že každá funkce toho programu skončí. Pokud mám funkci nastav_turbine_extra_dulezity_provozni_parametr(input), která má nějaký vstup, nelze (pro netriviální funkce) prokázat, že někdy skončí pro libovolný vstup. Takže nemůžu formálně prokázat, že je program pro ovládání turbíny správný a bude vždy fungovat.

[javaman ()]

možná jsem přízemní, ale k čemu to je dobré? znamené to že nejde ověřit (řekněme že skončí a že mu nepřetečou celočíselné proměnné) program na hlídání provozních parametrů turbíny?

Nelze ani ověřit, že každá funkce toho programu skončí. Pokud mám funkci nastav_turbine_extra_dulezity_provozni_parametr(input), která má nějaký vstup, nelze (pro netriviální funkce) prokázat, že někdy skončí pro libovolný vstup. Takže nemůžu formálně prokázat, že je program pro ovládání turbíny správný a bude vždy fungovat.

A koho to zajímá? Až začneš dělat reálné věci, tak na podobné nesmysly rychle zapomeneš.

[v]

možná jsem přízemní, ale k čemu to je dobré? znamené to že nejde ověřit (řekněme že skončí a že mu nepřetečou celočíselné proměnné) program na hlídání provozních parametrů turbíny?

Nelze ani ověřit, že každá funkce toho programu skončí. Pokud mám funkci nastav_turbine_extra_dulezity_provozni_parametr(input), která má nějaký vstup, nelze (pro netriviální funkce) prokázat, že někdy skončí pro libovolný vstup. Takže nemůžu formálně prokázat, že je program pro ovládání turbíny správný a bude vždy fungovat.

co je to u vás to "netriviální"?