#13: Rod Chapman – It's Either Automated or It's Wrong

Building Better Systems

Nội dung được cung cấp bởi Galois Inc., Joey Dodds, and Shpat Morina. Tất cả nội dung podcast bao gồm các tập, đồ họa và mô tả podcast đều được Galois Inc., Joey Dodds, and Shpat Morina hoặc đối tác nền tảng podcast của họ tải lên và cung cấp trực tiếp. Nếu bạn cho rằng ai đó đang sử dụng tác phẩm có bản quyền của bạn mà không có sự cho phép của bạn, bạn có thể làm theo quy trình được nêu ở đây https://vi.player.fm/legal.

2+ y ago 44:03

MP3•Trang chủ episode

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.

Watch all our episodes on the Building Better Systems youtube channel.

Joey Dodds: https://galois.com/team/joey-dodds/

Shpat Morina: https://galois.com/team/shpat-morina/

Rod Chapman: linkedin.com/in/rod-chapman-7b60266

https://github.com/rod-chapman/SPARKNaCl

Galois, Inc.: https://galois.com/

22 tập

#Tech #Podcasting Education #Government #Galois Inc #Joey Dodds #Shpat Morina