Very nice post thanks - I didn’t know about cakeml and bootstrapping formally verified compilers.