所以我看到一些人要求在塞耶龙（Ceylon）的工作开始于类型系统健全性的形式证明。因为我还没有一个，所以他们给我起了各种名字。我对这件事有点困惑，因为这是历史上第一次对一种用于实用计算的编程语言有这样的要求 :-)
尽管如此，我认为这个异议很有趣，值得某种形式的回应。所以这是我的看法。
首先，塞耶龙（Ceylon）有一个非常简单、超级传统的核心类型系统。在核心，系统仅仅是
- 参数化多态性加上方差注释，以及
- 混入继承。
现在，我们已经知道这个基本类型系统是健全的。其他人已经证明了这一点。事实上，如果我的理解正确，Scala 的人已经证明了加上混入继承和泛型的更复杂类型系统的健全性。
在语言规范中仅通过原始定义了五件事
- 联合类型，
- 具现泛型，
- 属性，
- 嵌套类，以及
- 高阶函数。
在塞耶龙（Ceylon）中看到的其他几乎所有东西都是在这个基本方案之上的糖衣：参数化多态性 + 方差注释 + 混入继承。我的意思是，你可以用这些更原始的概念重新表达语言中的其他构造。这就是规范定义它们的方式（偶尔可能需要一些解读字里行间的意思）。
这就是为什么Ceylon选择通过等价的Ceylon代码来指定像运算符这样的内容的原因之一。在类型系统中，我们没有任何特殊的空位
或原始的特殊情况
。没有原始的数值类型、数组、原始类型、内置类型提升或原始的null。甚至消除了重载，这确实似乎使正确性证明更加困难。
事实上，上面列出的大多数内容如果需要的话，也可以用更原始的概念来定义
- 接口的联合类型可以解释为
隐式
接口（但类的联合类型是个问题） - 具体泛型实际上意味着为泛型构造函数和方法添加一个额外的
隐式
参数（实际上，这也是在JVM上实现它的方式） - 属性可以被看作是在字段+方法上的语法糖（实际上，这也是在JVM上实现它的方式）
- 嵌套类可以被看作是在顶层类上的语法糖（实际上，这也是在JVM上实现它的方式）
- 高阶函数支持可以被看作是在特别生成的类上的语法糖（实际上，这也是在JVM上实现它的方式）
明白了吗？尽管这些内容在规范中是以原始术语定义的，但我们已经知道它们可以用其他原始构造来重新表达，因为我们已经需要能够做到这一点，以便将语言编译成Java字节码。
实际上，我相信很容易证明几乎任何Ceylon程序都可以机械地转换为一个具有参数多态+方差注解+混入继承的已知正确性语言。这个规范本身就足以作为Ceylon类型系统正确性的证明！
我有一个主要的疑问。我不确定之前研究过的类型系统是否包括联合类型。对于计算机科学学生来说，尝试将一些现有的正确性证明添加联合类型将是一个有趣的练习。不清楚是否有人已经做了。
无论如何，我想表达的观点是，你不需要一个从第一原理出发的完整形式证明来确保你的类型系统是正确的。如果核心类型系统已知是正确的，因为别人的工作，而且如果你知道某些其他结构可以用更简单的核心结构来重新表达，那么你就有了对该结构正确性的非正式证明。也许不足以作为学术论文，但足以开始编译器的工作。
你怎么看？我遗漏了什么吗？
