text: Transient gradual typing imposes run-time type tests that typically cause a linear slowdown in programs' performance. This performance impact discourages the use of type annotations because adding types to a program makes the program slower. A virtual machine can employ standard just-in-time optimizations to reduce the overhead of transient checks to near zero. These optimizations can give gradually-typed languages performance comparable to state-of-the-art dynamic languages, so programmers can add types to their code without affecting their programs' performance.
  @cite_25: There are several different gradual typing semantics, reflecting different trade-offs between performance and type soundness guarantees. Notably absent, however, are any data on which of these semantics developers actually prefer. We begin to rectify this shortcoming by surveying professional developers, computer science students, and Mechanical Turk workers on their preferences between three gradual typing semantics. These semantics reflect important points in the design space, corresponding to the behaviors of Typed Racket, TypeScript, and Reticulated Python. Our most important finding is that our respondents prefer a runtime semantics that fully enforces statically declared types.
  @cite_23: The literature on gradual typing presents three fundamentally different ways of thinking about the integrity of programs that combine statically typed and dynamically typed code. This paper systematically compares the theory of these approaches, their logical implications for the developer, and their performance.
  @cite_11: In order to aid in the process of detecting incorrect program behaviors, a number of approaches have been proposed which include a combination of language-level constructs (such as procedure-level assertions contracts, program-point assertions, gradual types, etc.) and associated tools (such as code analyzers and run-time verification frameworks). However, it is often the case that these constructs and tools are not used to their full extent in practice due to a number of limitations such as excessive run-time overhead and or limited expressiveness. Verification frameworks that combine static and dynamic techniques offer the potential to bridge this gap. In this paper we explore the effectiveness of abstract interpretation in detecting parts of program specifications that can be statically simplified to true or false, as well as the impact of such analysis in reducing the cost of the run-time checks required for the remaining parts of these specifications. Starting with a semantics for programs with assertion checking, and for assertion simplification based on static analysis information, we propose and study a number of practical assertion checking modes, each of which represents a trade-off between code annotation depth, execution time slowdown, and program safety. We also propose techniques for taking advantage of the run-time checking semantics to improve the precision of the analysis. Finally, we study experimentally the performance of these techniques. Our experiments illustrate the benefits and costs of each of the assertion checking modes proposed as well as the benefit of analysis for these scenarios.
summary: The diversity of semantics and language designs incorporating gradual typing has been captured recently via surveys incorporating formal models of different design options. Chung et al. present an object-oriented model covering optional semantics (erasure), transient semantics, concrete semantics (from Thorn @cite_11 ), and behavioural semantics (from Typed Racket), and give a series of programs to clarify the semantics of a particular language. Greenman et al. take a more functional approach, again modelling erasure, transient ( first order''), and behavioural ( higher order'') semantics @cite_23 , and also present performance information based on Typed Racket. Wilson et al. take a rather different approach, employing questionnaires to investigate the semantics programmers expect of a gradual typing system @cite_25 .