Názor k článku HelenOS nikdy nebude dokončený, říká jeho autor Jakub Jermář od M.D. - Obavam se ze pokud bude projekt psan v...

Obavam se ze pokud bude projekt psan v C/C++, tak "pokusy o formalni verifikaci spravnosti kodu" zustanou jenom pokusy

Problém není v programovacím jazyku, ale v množství abstrakce a sémantické informace, která je v kódu nějak implicitně nebo explicitně obsažena. Souhlasim, že lze asi s jistou básnickou licencí obecně říci, že Java se verifikuje snadněji než C a funkcionální jazyky se verifikuji snadnějí než imperativní jazyky, ale v praxi jde vždy o to, jaké vlastnosti a jakým způsobem chcete verifikovat, jak se poperete s nerozhodnutelností a state space explosion apod.

Nástroje pro formální verifikaci céčka existuji, např. Frama-C, VCC.

Neuvazovali jste treba o nejakem kulturnejsim (rekneme funkcionalnim) jazyku?

Nevidím na céčku nic nekulturního. Každý programovací jazyk lze používat kulturním i nekulturním způsobem.

Ovšem budoucímu použití nějakého funkcionálního jazyka nebo alespoň imperativního jazyka s funkcionálními prvky (typu Groovy) se rozhodně nebráníme. Až budeme umět chodit, můžeme se učit běhat :)