4 ms·
How's this for interesting: many people in my field (formal methods) seem to be pretty excited about our job prospects. Before we used to just say that people d
by markusde 3y ago
How's this for interesting: many people in my field (formal methods) seem to be pretty excited about our job prospects. Before we used to just say that people don't actually know what their code does, but now it looks like it might really be true.
- trealira 3y ago> How's this for interesting: many people in my field (formal methods) seem to be pretty excited about our job prospects. Wow, I hadn't thought of it from the generative AI standpoint, only from the standpoint of "cybersecurity is increasingly important, so we need to use proof assistants and verified toolchains more". What kind of new career prospects in formal methods do you predict will come as a result of generative AI? For example, certifying AI-generated code for use in automobiles?
- markusde 3y agoFull verification is one, but that is still challenging at scale. Formal methods has many weaker methods as well which are easier to apply in general (automated proof, abstract interpretation, static or dynamic model checking, hell some would even argue the judicious use of dynamic checks is a kind of formal methods). I think that a shift from "this is my program, it's a sequence if steps that does what it does" to "I asked a LLM to generate me a program that does this vague thing I want" makes you naturally ask questions like "wait is it actually doing the thing I want" and "what do I even want it do do". Formal methods, broadly, has a lot of good answers to those questions.
- diarrhea 3y agoIt’s true. We don’t. But does it matter? Is there demand to change this?