Comment on We did this to ourselves
deegeese@sopuli.xyz 11 months agoThe problem with formal proofs for code is that it assumes the spec/ requirements are complete and big-free.
I find most bugs come from missed or misinterpreted requirements.
Comment on We did this to ourselves
deegeese@sopuli.xyz 11 months agoThe problem with formal proofs for code is that it assumes the spec/ requirements are complete and big-free.
I find most bugs come from missed or misinterpreted requirements.
tatterdemalion@programming.dev 11 months ago
I have a feeling you are misunderstanding what is meant by “theorem” here. For example, one theorem that is proven by all safe Rust programs is that they are free of data races. That should always be a requirement for functional software. This is a more pragmatic type of automatic theorem proving that doesn’t require a direct proof from the code author. The compiler does the proof for you.