Programming Language for Effective and Reliable Software Development

为了提高软件开发的效率，同时保持产品的可靠性，我们开发了一种新的编程语言，它同时支持类型安全(在程序执行前检测与类型相关的错误的能力)和可伸缩模块化(从软件模块构造产品的能力，这些模块也是从其他细粒度模块构造的)。我们还开发了一种支持动态模块组合和分解的编程语言，实现了一种新的程序验证机制。

To enhance effectiveness of software development while preserving the reliability of products, we developed a new programming language that supports both features of type safety (ability to detect type-relating errors before program execution) and scalable modularity (ability to construct products from software modules, which are also constructed from other fine-grained modules). We also developed a new programming language that supports dynamic module composition and decomposition, and realized a new mechanism for program verification.