A fundamental belief underlying forty years of programming languages research, aptly captured by the slogan
“Well-typed programs can’t go wrong”
, is that programs augmented with machine-checked annotations are more likely to be free of bugs. But of course, real programs do wrong and programmers are voting with their feet. Dynamic languages such as
are unencumbered by redundant type annotations and are increasingly popular.
of the web, is moving to the server with the success of
, another dynamic language, is being used in statistics, biology and finance for data analysis and visualization. Not only are these languages devoid of types, but they utterly lack any static structure that could be used for program verification. This talk will draw examples from recent results on
to illustrate the extent of the problem and propose some directions for research.