Formálně dokazatelné programovací jazyky jsou jen esoterickou myšlenkou matematiky / CS, která se do reálného světa nepřekládá dobře. Jednoduše se neškálují pro praktický kód. Realita je taková, že pokud chcete vybudovat úspěšný vývojářský ekosystém, váš jazyk musí být více podobný JavaScriptu než Haskellu. To platí zejména s nárůstem LLM, kde jazyky s větším množstvím tréninkových dat budou neustále zvyšovat svůj podíl na trhu. Říkám to jako někdo, jehož oblíbeným programovacím jazykem byl Haskell a který vyvinul tyto systémy od začátku do konce, od návrhu jazyka až po kompilátory a dokonce i základní matematické řešiče. Neškálují se, protože základní matematické řešiče exponenciálně explodují.