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
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