据 Woofun AI 消息，以太坊联合创始人 Vitalik Buterin 提出一种新型高级编程语言构想。该语言可编译为 Lean 或 HOL 等格式，核心设计目标是优化定义与定理的人类可读性，而非证明过程。