Виталик: Новые виды продвинутых языков программирования стоит попробовать, они должны облегчать чтение определений и теорем.

Odaily сообщил, что Vitalik опубликовал сообщение на платформе X, в котором он отметил, что новый тип «продвинутого языка программирования», который стоит попробовать — это язык, компилируемый в Lean (или HOL и другие), с акцентом на максимально удобочитаемое определение и теоремы для человека. Не доказательства, поскольку главное — чтобы доказательство было верным; основное — это сами определения и теоремы. Предполагаемое применение: ИИ генерирует длинный блок доказательства, а читателю нужно максимально просто понять, какие конкретные утверждения в этих доказательствах действительно были доказаны.