资 源 简 介
Numerous approaches to the problem of determining the correctness of computer programs have been proposed and implemented, such as dynamic and static type checking. Static typing enables earlier error checking and more efficient execution in many programs, while dynamic type systems allow for greater expressiveness and flexibility. This project presents a type system, hybrid typing, and a programming language utilizing it, Gnarly, that negotiate the space between static and dynamic typing by allowing the programmer to select which typing paradigm he or she wishes to use at the level of individual terms rather than entire languages. Furthermore, any program in Gnarly that is entirely static is provably type safe, and therefore is inherently more trustworthy than it would be otherwise. This results in a very robust language, capable of expressing a wider range of possible programs than any static language, but still retaining a far stronger degree of reliability and security than is a
