#13: Rod Chapman – It's Either Automated or It's Wrong
Building Better Systems - Un pódcast de Galois, Joey Dodds, Shpat Morina
Categorías:
Rod Chapman explains his recent verification of TweetNACL using SPARK/ADA. We discuss how every aspect of his proofs are automated, how the correctness proofs actually enabled better performance after compilation, and higher confidence in some otherwise risky-seeming optimizations.
