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.