The Supervisionary proof-checking kernel (or: a work-in-progress towards proof generating code)