One of the research organizations using CakeML is MIRI (Machine Intelligence Research Institute), which is doing research in machine self-reference. They recent

One of the research organizations using CakeML is MIRI (Machine Intelligence Research Institute), which is doing research in machine self-reference. They recently used HOL, an automated theorem prover, to demonstrate a formal correspondence between the model of HOL within HOL (“inner HOL”) and HOL itself (“outer HOL”). Informally speaking, Fallenstein and Kumar show that one can always build an interpretation of terms in inner HOL such that they have the same meaning as terms in outer HOL. The authors then show that if statements of a certain kind are provable in HOL’s model of itself, they are true in (outer) HOL. See more here: https://intelligence.org/2015/12/04/new-paper-proof-producing-reflection-for-hol/ https://intelligence.org/2015/12/04/new-paper-proof-producin...