SHF: Medium: Collaborative Research: Semantics Engineering for Scripting Languages

在过去的十年中，脚本语言扮演了巨大的角色。最初，Web开发人员使用Perl和Python来丰富Web服务器的内容；后来Ruby on rails掀起了一场风暴。在同一时期，JavaScript已经成为Web客户端的主导语言。此外，脚本语言的流行激发了开发人员使用脚本语言来构建许多其他类型的系统，包括任务关键型实时系统。尽管脚本语言是探索设计思想的高效工具，但它们的使用也给软件周期带来了一些新的问题。最基本的是，脚本语言往往缺乏类型系统，这往往会增加系统的调试和维护成本。更糟糕的是，尽管脚本语言往往是安全的，但它们灵活的原语操作在程序中会导致难以预测的行为，从而产生新的安全漏洞。同时，脚本语言没有良好定义的语义，这使得几乎不可能验证程序安全或安全属性分析的可靠性。具体地说，PI建议研究三种脚本语言的可执行语义的构造：JavaScript、Python和Racket。他们将使用语言级测试套件来检查语义是否对实现进行了充分的建模。此外，PI将使用语义来设计和验证这些脚本语言的类型系统和程序分析。从长远来看，这项提议应该会在三个方面影响整个世界。首先，脚本语言的类型系统和分析应该帮助软件开发人员提高他们软件的安全性，降低他们的维护成本。其次，脚本语言的语义将帮助研究人员验证他们关于程序分析的想法。最后，PI将开发一个语义重新设计的流程，该流程应该对许多其他脚本语言社区有用。

Over the last decade, scripting languages have assumed a huge role. Initially web developers used Perl and Python to enrich the content of web servers; later Ruby on Rails took the scene by storm. Over the same period, JavaScript has become the dominant language on the client side of the web. Additionally, the popularity of scripting language has inspired developers to use them for the construction of many other kinds of systems, including mission-critical real-time systems. While scripting languages are productive tools for the exploration of design ideas, their use also introduces several new kinds of problems into the software cycle. Most basically, scripting languages tend to lack a type system, which tends to raise the debugging and maintenance costs for systems. Worse, even though scripting languages tend to be safe, their flexible primitive operations induce difficult-to-predict behavior in programs and thus creates novel kinds of security holes. At the same time, scripting languages do not come with a well-defined semantics, making it nearly impossible to validate the soundness of a program analysis for safety or security properties.In response to these observations, this proposal promises to re-engineer the semantics of scripting languages. Specifically, the PIs propose to investigate the construction of executable semantics for three scripting languages: JavaScript, Python, and Racket. They will use the language-level test suites to check that the semantics model the implementations adequately. In addition, the PIs will use the semantics to design and validate type systems and program analyses for these scripting languages. Over the long run, the proposal should impact the world at large in three ways. First, the type systems and analyses for scripting languages should help software developers improve the safety of their software and reduce their maintenance cost. Second, the semantics for the scripting languages will help researchers validate their ideas concerning program analyses. Finally, the PIs will develop a process for semantic re-engineering that should be useful to many additional scripting language communities.