In every proof assistant something is doing all that logic, whether you call it a kernel or not. As I understand their writing, ML is a language meant for deve

In every proof assistant something is doing all that logic, whether you call it a kernel or not. As I understand their writing, ML is a language meant for developing proof assistants and this debate is specific to proof assistants written in ML, about the extent to which you use ML's type system as part of the kernel (proofs or theorems are types, at least partially), or write one yourself (proofs are just objects). Even Rust has an unsound type system that allows arbitrary memory access in safe code, so you can't just assume your programming language has a sound type system.