Názor k článku Statické typové kontroly zdrojových kódů Pythonu prováděné nástrojem Mypy od Calculon - Formální verifikace je nadmíru praktická. Ty pokročilé vlastnosti...

Formální verifikace je nadmíru praktická. Ty pokročilé vlastnosti a konstrukce, které běžný vývojář (třeba Ink, jak nám tu sám přiznal) nechápe, se beztak používají hlavně v knihovnách, aplikační kód se píše jednodušeji, už jen kvůli čitelnosti. U typových systémů se formálně (teoreticky) silný a praktický nevylučují, spíše naopak.

BTW OCaml je na dobré cestě k lepšímu překladači. Haskell nekomentuji, ten má tolik volitelných rozšíření, že už jsem ztratil přehled.