As programming languages researchers, we are interested in designing beautiful abstractions, which enable sound reasoning and construction of safe systems. But ultimately, human beings employ those abstractions to construct systems in ways that make sense to them. HATRA (Human Aspects of Types and Reasoning Assistants), which debuted at SPLASH 2020, is a new workshop intended to build community and establish a research agenda on this topic. A group of thirty researchers and software engineers convened over two days to discuss the relationship between formal approaches and programmers that use them.
Read in full here:
This thread was posted by one of our members via one of our news source trackers.
1 Like
Corresponding tweet for this thread:
Share link for this tweet.
1 Like
Python, a dynamically typed language, has become very popular in introductory programming courses. If static types are helpful for programming, are they not also helpful for beginners? One hypothesis is that introducing a type system requires people to learn two notional machines (the type checker as well as the operational semantics) rather than just one, making learning the language harder. Is this right? How can we design type systems that we can show benefit beginners as well as experts? Or, alternatively, of the many different programmers doing different things, which might be better off starting with a strongly typed language?
Maybe a language where the type system is also defined in the language? Like Idris but more homoiconic?
1 Like
But OCaml and Rust infer types pretty well so people can avoid writing type annotations and still get quite far.
But yeah, it doesn’t nullify the argument that people have to be aware of the types of data they’re working with regardless.
2 Likes
