I just published the second blog post in my series about Candid: In
https://www.joachim-breitner.de/blog/783-A_Candid_explainer__Safe_higher-order_upgrades
I explain how Candid supports higher-order function composition, give a general framework to analyze such IDLs, and finally show off with our Coq formalization of that.
The next post will have to wait for a few days, as I’ll be away from my laptop.