Vitalik: Нові мови високорівневого програмування, які варто спробувати, повинні робити визначення та теореми легшими для читання

Odaily повідомляє, що Vitalik опублікував допис на платформі X, у якому зазначив, що одним із напрямків, який варто спробувати у нових "просунутих мовах програмування", є створення мови, яка компілюється у Lean (або HOL тощо), з акцентом на максимально легке для людини читання визначень і теорем. Мова йде не про доведення, адже важливо тільки їхню коректність, а саме про визначення та теореми. Передбачається, що AI створює великий обсяг доведень, а читачу слід мати змогу якнайзручніше зрозуміти, які саме твердження в цих доведеннях було доведено.