3 ms·
I’m new to this space so I’m not sure how PLT is distinct from formal verification, but my view of it is that formal methods are another form of testing. Unit t
by ragona 7y ago
I’m new to this space so I’m not sure how PLT is distinct from formal verification, but my view of it is that formal methods are another form of testing. Unit testing also does not guarantee that you’re testing the right things, but it’s a good way to catch issues post-compile but pre-release. Formal verification moves that so that you catch issues as part of the compilation step, which is just another tool in the general toolbox of finding errors before you ship them to your users. It’s not about proving that your spec is good, it’s about automatically generating tests that find certain types of bugs.
- pron 7y agoFormal methods are a large set of methods that allow you to analyze a program in ways that can verify it satisfies certain (correctness) properties. Most formal methods don't generate tests (although some do), but the term "compile-time" is not often used, as most formal methods are not part of the compiler. There is some overlap between PLT and formal methods, as that some concepts studied in PLT -- most notably type systems -- can be used for formal verification, but the main thrust of formal methods uses other techniques. Both disciplines heavily rely on formal logic.