Scripting languages such as Python, Javascript, and Ruby have carved out an important niche: rapid development of solutions to small and medium sized problems. Unfortunately, scripting languages today also have significant shortcomings: type errors arise only at runtime, making it harder to isolate bugs; there are no declared type interfaces, forcing libraries to use informally-described interfaces; and runtime performance is poor compared to statically-typed languages. The main cause of these problems is the lack of a static type system.
This project is preliminary work on a new scripting language that addresses this problem by developing a statically-typed scripting language from scratch, aiming to retain the flexibility of existing scripting languages while also solving the fundamental problems of difficult debugging and poor runtime performance. The PI's approach is based on subtype constraint type inference algorithms, which are very flexible and do not require type declarations.
Programming language technology underlies all modern computation tasks and is thus pervasive through society. Even a small improvement to this base will lead to broad impacts on society since a single programming language may be found on large servers, in laptops, on cellphones, and in robots, cars, and other devices. For example, if a given program can be made to run faster the computer may require less power; currently around 5% of the US power consumption is to power and cool computers. If a programming language is more productive in that programmers using it finish their tasks more quickly and produce more reliable code it will have a pervasive impact on programmer productivity and software quality and security. The goal of the Big Bang project is to develop fundamental new technologies for this purpose: to develop new programming language principles to build languages that achieve an improvement in both flexibility and efficiency compared to existing programming languages. The particular sort of existing language we focus on are so-called scripting languages, programming languages such as Python, Javascript, Ruby, etc, that were designed to be very flexible and to support fast programming of small tasks. As scripting languages evolved they have been used for larger and larger tasks, but their lack of runtime efficiency and lack of early reporting of type errors make them less than ideal for such tasks. Our primary focus has been the development of novel principles for enabling a compiler to automatically find a wide class of errors in such programs. Our secondary focus has been developing fundamental new principles for compiling such programs which will lead to significantly faster run-time lookup of data and thus much faster performance overall. In the period funded by NSF we made significant refinements and extensions to earlier ideas. One problem with powerful fully automatic analysies is that the complexity becomes overwhelming; we spent considerable time developing a much more concise account of the underyling theory which makes the underling principles more apparent. We also developed several extensions, including added expressiveness features for programmers and a means whereby programmers could assert automatically verified type invariants.
