4 ms·
I believe type sytems/type theory is likely going to be the most popular method for formal verification of programs (aka static analysis). And of course, there'
by thekhatribharat 7y ago
I believe type sytems/type theory is likely going to be the most popular method for formal verification of programs (aka static analysis). And of course, there's a limit to what you can prove about programs (ref: Rice's theorem).
- jfkebwjsbx 7y agoStatic analysis is not formal verification.
- thekhatribharat 7y agoSure, things like enforcing style guides, etc. can be seen as lightweight formal verification.
- irundebian 7y agoYes, but you wrote "formal verification of programs (aka static analysis)". Formal verification is not also known as static analysis.
- exdsq 7y agoIt's part of the field of formal methods.