在编程语言的世界中，逻辑表达通常以布尔类型（boolean）为基础，即真（true）或假（false）。然而，TypeScript和Lean语言在逻辑表达的处理上展现出截然不同的哲学。TypeScript沿袭传统，将逻辑表达式视为布尔类型，而Lean语言则创新性地将诸如“2 + 2 = 4”这样的逻辑语句视为一种独特的类型——命题（Prop）。这种设计使得Lean能够实现“类型化真实性”，即在程序中确立事实并安全地传递它们。这一差异不仅体现了编程语言设计的多样性，也为形式化验证和数学证明提供了更强大的工具。Lean的这一特性使其在学术界和需要高可靠性验证的领域备受关注，展示了编程语言理论的前沿发展。