spir: > First, "eat your own food". Right, but in the case of the SPARK compiler the main purpose of writing it in SPARK + full proofs is probably to not introduce bugs in user code caused by compiler bugs. Bye, bearophile