Re:Advent of Code 2018, in Coq
by nickpsecurity on Monday February 18, 2019 @07:34PM
(#19195780)
" with the hope that the compiler will direct one towards the bugs and they will be easier to find."
Also, less expensive to fix given bugs are cheaper to fix earlier in the lifecycle. You can also reduce breakage during changes to existing code. Finally, you can warranty the code at specific defect rates or for certain kinds of defects where the fixes are free within the warranty. Companies using Cleanroom and Correct-by-Construction did that with the above benefits.
Also, less expensive to fix given bugs are cheaper to fix earlier in the lifecycle. You can also reduce breakage during changes to existing code. Finally, you can warranty the code at specific defect rates or for certain kinds of defects where the fixes are free within the warranty. Companies using Cleanroom and Correct-by-Construction did that with the above benefits.
http://infohost.nmt.edu/~al/cseet-paper.html
http://www.anthonyhall.org/c_by_c_secure_system.pdf