This is one actual use of SPARK for me. Prove the absence of runtime errors (and if necessary add preconditions) then let the compile optimize to hell. Another

This is one actual use of SPARK for me. Prove the absence of runtime errors (and if necessary add preconditions) then let the compile optimize to hell. Another example on tweetnacl: https://blog.adacore.com/sparknacl-two-years-of-optimizing-crypto-code-in-spark-and-counting https://blog.adacore.com/sparknacl-two-years-of-optimizing-c...