Formal 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

Formal 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.