The job of a software engineer is not to produce code, but to solve problems; we just happen to solve most of those problems by producing code. Ultimately, producing code is hard, and we need help. That's why GitHub's Copilot is exciting, but it's far from ideal, and it's the tip of the iceberg of what's been done and what is to come.

There have been a lot of hot takes on Copilot specifically, so I'm not going to get into the flaws of this specific launch very much (ethical issues, introducing bugs, etc). At the end of the day, it's pretty exciting, and it's flawed like all tools based in statistical inference are. (This is a very important area and there is a lot of room for people to make huge strides forward in HCI and UX around ML.) It's helpful because it can reduce the friction of producing code, which is a necessary but ultimately small part of the job of a software engineer. And it's only doing one part of what we do when we code!

The usual process for coding (for me) looks something like this:

• Specify: Figure out what the code needs to do
• Implement: Write the code in question
• Verify: Test the code to make sure it does what it needs to
• Iterate: Rinse and repeat as many times as needed (incremental development, fixing bugs, etc.)

And that's skipping all the work needed to gather requirements ahead of time; that's just the coding part.

So Copilot, and other code generation tools I've seen, handle the implementation bit: they write the code in question, and make no attempts at or guarantees around correctness or completeness. It's a starting point, and that's great. It really emphasizes, though, how much we need to focus on the specification and verification steps. If we have easy code generation available, it's very easy as a human under pressure to ship code quickly to just say "looks good to me" and ship it. That's how you get subtle bugs and omissions, and in the long run that's just programming, and misses the whole engineering part.

Wouldn't it just be grand if we could write a spec for some piece of code, then let the machines do the rest? I know, I know, people have been trying that for a long time and it's fraught. I'm not saying we can do that, theoretically or practically, today or in ten years. But as a goal, that's really what you want: we want to solve the problem by saying "this is the solution" and then poof the solution appears! To some people, Copilot will feel like exactly that magic, and that's dangerous. It skips the verification step, and I'd argue it also skips specifying what you want (because a docstring is often not very clear, ambiguous, and misses the non-functional components that are oh-so-important like performance and security).

So, where does that take us? Well, we want to do engineering to solve problems. I think that means, practically speaking, we need to focus on the specification and verification steps and nail down better methods for doing that, while also working to improve the tooling for implementation (better autocomplete, code generation, etc). If we can improve the specification and verification steps, we'll get a lot more mileage out of flawed implementation tools and techniques, and we'll be able to move faster on the implementation step regardless because we'll know that we can move quickly and make mistakes since they'll get caught. Good specification and verification speed up the implementation portion while giving you better outcomes all around.

The future of software engineering is leaning into formal methods and relying on formal methods to give us higher quality output.

And the future is here, somewhat! There are already tools you can use to more rigorously specify and verify your code and systems:

• TLA+ is the elephant in the room, and has been used quite a bit to verify systems at AWS and MS, among others; probably a good starting point!
• Property testing (things like Hypothesis for Python) is also a form of formal methods that can take you very far and is low hanging fruit if you already have unit tests. It lets you get higher levels of assurances while not having to fully formally verify your program.
• Even static types are a form of formal methods, and they're increasingly being embraced even in languages like Python and Ruby! In the future we can take it further with refinement types to get nice strong compile-time guarantees around values.
• Many more which I'm not aware of, because I'm new to this area. (Email me or tweet at me with recommendations!)

That's not to say that all code will need or benefit from formal methods; some one-off scripts or simple web apps can be crafted without it, and would be too expensive using formal methods. That's fine, and that indicates that there's a split in our field: software engineering vs. software development. This rift will probably become more clear over time, as well, as we figure out ways of talking about the engineering side of software engineering and better ways of specifying and verifying our programs.

I'm leaning into this, personally. I tend to work on things where correctness, stability, reliability, and security are all very important, so formal methods give a way to improve this work and deliver on those values. First on my learning list is TLA+.

If you have any experience with this stuff, have recommendations of what to learn, or just want to chat about it, reach out to me by email or on Twitter. I'd love to chat about it!