This is what I wish for in an IDE in the future: <a href="https://twitter.com/TaliaRinger/status/1365433319572185092?s=20" rel="nofollow">https://twitter.com/TaliaRinger/status/1365433319572185092?s...</a><p>The year is 2030. You're a software engineer at a company, writing tests for your program.
After you write a few tests, your IDE is like, "hey, I noticed you were testing this; do you want this more general thing to hold?" and spits back a specification for you. You're not sure.
You say, "give me some examples," and your IDE generates more tests for you. One of them looks off, so you tell your IDE, "no, not that one."
Your IDE sends you another specification. This one looks better, so you approve it. Your IDE tells you to hang out for a bit while it tries to see if it actually holds.
After ten seconds or so, it generates a failing test. You fix your code and try again.
This time it's like, "I couldn't find any counterexamples, but I'm also not positive it's true. Can you help me prove it?" You say yes, of course.
It asks you a couple of specific questions about your code. Thinks for a bit, and then tells you that your code is verified.
In fact if you are an advanced user you can go check out the proof yourself. No need to, though.
A couple of days later, you change your code. Your IDE notices this and tries to check the specification again. It tells you that it is no longer true; but based on the change you made, there is an analogous change in the specification, so maybe you want this new specification?
You're not sure so you ask for some tests. It looks good. And this time the tool doesn't need to ask you any questions to prove it; the proof is similar enough to the proof of the old specification, so you're good.
After a few more weeks of this, your IDE notices something else, though. You keep changing that function, and changing your specification to go with it.
So it recommends a new abstraction for you that would have captured all of the past examples. It tells you, hey, if you use this, things might break less often to begin with .
It looks good so you're like, "oh cool, yeah let's do that." And it drops into a guided refactoring mode, helping you through the change, asking you just a few questions but automating all of the tedium.
Does this for your program, then for your proof. And your proof doesn't break again for months after that. Good shit.