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

Reply via email to