For me, Composita https://concurrency.ch/Content/publications/Blaeser_Component_Operating_System_PLOS_2007.pdf https://concurrency.ch/Content/publications/Blae

For me, Composita https://concurrency.ch/Content/publications/Blaeser_Component_Operating_System_PLOS_2007.pdf https://concurrency.ch/Content/publications/Blaeser_Componen... and ASAP https://www.semanticscholar.org/paper/ASAP%3A-As-Static-As-Possible-memory-management-Proust/4eb76f9a5b8874328773bf189a22b0975401f373 https://www.semanticscholar.org/paper/ASAP%3A-As-Static-As-P... Seem like a good way forward wrt memory management and concurrency, using ASAP inside a component, and delegating concurrency and component cleanup to Composita. Other languages like Maude http://maude.cs.illinois.edu/w/index.php/The_Maude_System http://maude.cs.illinois.edu/w/index.php/The_Maude_System Are pushing in new directions wrt proof checking.