Asynchronous code is remarkably hard to get right, making it a common source of errors in TypeScript code. However, we would not be able to write TypeScript applications without it, because it enables long-running actions without freezing the current view. Developers usually rely on manual inspection to understand it, which is quite painful: tracing the order in which callbacks are called may involve various modules or dependencies. These difficulties also make automated reasoning of asynchronous code hard.
In this talk, I present a backward goal-directed static analyser to verify provable assertions in TypeScript programs involving asynchronous calls. The goal is to verify that the assertion always holds for all reachable program locations. To do so, an abstraction of the provable assertion is propagated backwards through the program. In order to scale, the analysis only needs to visit the portion of code that is relevant for proving the assertion. A preliminary implementation built on top of a previous tool called TajsVR demonstrates the feasibility of the approach on TypeScript applications. Showing how this analyser can be used to encode business logic knowledge that would otherwise be propagated via comments or documents — and eventually lost.
