Мови програмування з формальними доказами – це просто езотерична ідея Math / CS, яка погано перекладається на реальний світ. Вони просто не масштабуються для практичного коду. Реальність така, що якщо ви хочете створити успішну екосистему розробників, ваша мова має бути більше схожа на JavaScript, ніж на Haskell. Це особливо актуально з ростом LLM, де мови з більшою кількістю навчальних даних продовжуватимуть збільшувати свою частку ринку. Я кажу це як людина, чиєю улюбленою мовою програмування була Haskell і хто розробляв ці системи від початку до кінця, від дизайну мови до компіляторів, і навіть до базових математичних розв'язувачів. Вони не масштабуються, тому що базові математичні розв'язувачі вибухають у геометричній прогресії.