Our great sponsors
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
Well, by this I mean math (and mathematical logic). Math is the tool for reasoning about possibly infinite concepts, i.e. you can make a statement about infinite sets and still know if it’s true or not. We aren’t limited to what we can see and touch, which is good because any non-trivial software application is so large that it could never be drawn out like a building blueprint. It can only be described and reasoned about abstractly.
But, you are probably asking about what ‘tools’ can be applied to programming, meaning some kind of library or application. These are also out there. Here’s a few that I think are promising:
TLA+: This is a specification language for describing and reasoning about computations as state machines, with a particular focus on modeling distributed systems. It has been used at Amazon to check designs for their distributed algorithms. They have used it to check parts of S3 for example: https://lamport.azurewebsites.net/tla/formal-methods-amazon....
Best reference is the book Specifying Systems: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf.
Then you have theorem provers / proof assistants based on type theory. These are frankly complex, but getting better.
F*: This one is the most exciting to me. It’s currently being used to develop a formally verified HTTPS stack: https://project-everest.github.io/. They already have components released to the Linux kernel and Firefox. One of the most exciting things about this tool is that you can verify an efficient, stateful algorithm and extract highly performant C code from it. Their verified implementations have equal or better performance to the current solutions out there. So all of the overhead is for verification, none exists at runtime.
Of course you can’t talk about proof assistants without mentioning Coq. Its claim to fame is producing a formally verified C compiler, CompCert: https://compcert.org/.
As you can see, so far, formal verification has been mostly limited to components of systems, not entire systems. But, it’s a start, and the scope of what we can verify is getting larger.