A while back I interviewed a coauthor of this paper here: https://www.youtube.com/watch?v=rqArTpY_kNY https://www.youtube.com/watch?v=rqArTpY_kNY We discussed

A while back I interviewed a coauthor of this paper here: https://www.youtube.com/watch?v=rqArTpY_kNY https://www.youtube.com/watch?v=rqArTpY_kNY We discussed the language he's helping develop (Granule) and which the concepts in this paper are implemented in. I actually asked him if he thought something like this paper would be possible and IIRC he said he was hopeful. I think listening to the interview would be a good way to get a feel for the big ideas. To get deeper into it, I'd recommend learning Haskell at least up to the point where you understand typeclasses, functors, and monads. That will get you familiar with some relatively advanced type system features. Granule is a research language so it has additional stuff going on, but that is a solid foundation. After that, just google terms you don't know (e.g. modal type theory) or look at the papers that are cited. You can also join the PLTD discord server, there are lots of type nerds in there who are usually happy to answer questions.