That’s right, you. The software engineer who hasn’t taken a logic or formal methods course. You already know formal methods. Sure, you might not be able to build a fancy new proof tool this month, but skills you apply every day are the building blocks of formal methods.
What gives? People do PhDs in formal methods after all.
It’s pretty common to see people asking “how do I get started in formal methods?”. There are often suggestions to read books that people might study in school, or papers, or to run through tutorials for popular tools. We’ve even got our own such tutorial, although that won’t be the right starting point for most people. Honestly, it’s not the right starting point for anyone. It’s great, don’t get me wrong, but I won’t pretend anyone should be starting formal methods with SAW.
Before we start with the next steps, let’s explain what you already know.
Sometimes you think you write correct programs
If you’ve put software into production, hopefully, hopefully occasionally you believe that it’s correct, or at least partially correct. Fine, I’ll settle for not disastrously wrong, schedules are tight. Not wrong might mean quite a few things. Maybe you believe that it:
- Doesn’t crash
- Always checks error codes
- Always fills a specific field with a specific value
Getting to the point where you believe any of these things is a huge accomplishment. You need a mental model of the programming language, a mental model of the program, and a mental model of the dependencies and external interactions of the program.
Formal methods is writing those models down and making use of them.
That’s not to say it’s easy, but it’s not nearly as far of a reach as it might feel when you’re staring down Software Foundations or the tutorials for the latest proof tool (and there are many of these). And there’s great news. As a formal methods user, you should be able to reuse lots of existing work to get what you need.
But you don’t even need tools to get started. You need a blank document. Pick a program, and write down what it should do. This is a pretty common step and you might do this all the time in your comments.
Once you know what it does, try to build up an argument for why you believe it does this. You’ll pretty quickly see how many rabbit holes there are, and that’s fine. Your program that uses a JSON parser is probably only correct if the JSON parsing library is correct (it isn’t). Documenting that risk is a valuable part of what formal methods can accomplish.
A common pattern is that correctness will depend on inputs in a way the type system can’t specify. For example, “If this function is provided with a valid JSON string, it will get the field called “name” and return it”. That’s great too! It helps users of your code (including yourself next week) learn when the code does the right thing.
Go try, please
It’s not very easy to do things, and even harder to do things differently. If you think you can, though, get a piece of paper or a doc and write down what you want your software to do. Then write down why you think it does this. Here are some things that might happen:
- You get a nice little doc you can drop in your repository
- You think of a time your software isn’t doing what you want it to do
- You write down something you already know and have documented
These are all fine outcomes. After 15 minutes you can walk away from it. The next time you come back, either pick a different piece of code or try to refine your arguments from the first time around. The more you can repeat this process, the better your software will be.