I've replied to Nix. The work is nice, no doubt, but it still requires 1 absolutely
trusted compiler, which would have to be written (or verified/assumed), as I
think you note. No doubt the work could be extended such that Ct is a set of
Do you think the "Fully" in the title of your thesis is perhaps unfortunate
though? Your work seems to re-enforce Thompson's result rather than fully
counter it, surely?