Re:Software engineering research is a train wreck
by hwayne on Tuesday July 20, 2021 @04:26PM
(#27898841)
Purely from an industrial perspective, interest in formal methods tends to split two ways:
1. Verifying really nasty algorithms, the kind you see in cryptography and embedded systems and stuff where the bugs are triggered by horrific race conditions or incredibly specific malicious inputs that even experts won't think of testing
2. High level specifications of requirements and abstract machines and stuff, where the spec is like 100 lines and the implementation is 10k and you'd prefer to catch some design bugs before you're ten sprints into coding
A lot of bugs in (1) end up being memory-related, which is why you're seeing languages with borrow checking as part of the semantics (Rust). A lot of hype these days is in (2) because it's a lot cheaper and easier to learn, at the cost of having a lower power ceiling.
1. Verifying really nasty algorithms, the kind you see in cryptography and embedded systems and stuff where the bugs are triggered by horrific race conditions or incredibly specific malicious inputs that even experts won't think of testing
2. High level specifications of requirements and abstract machines and stuff, where the spec is like 100 lines and the implementation is 10k and you'd prefer to catch some design bugs before you're ten sprints into coding
A lot of bugs in (1) end up being memory-related, which is why you're seeing languages with borrow checking as part of the semantics (Rust). A lot of hype these days is in (2) because it's a lot cheaper and easier to learn, at the cost of having a lower power ceiling.