A rich source of inspiration in programming languages is the correspondence between propositions and types. We look back at how modal operators such as necessity and possibility can help us understand computational phenomena through this lens. We then look forward and examine how recent discoveries regarding modalities might influence our thinking about advanced type systems.