Before I begin - I hope my comment doesn't come across as too confrontational. I don't want to invalidate your experience, but I'd like to spread information about formal verification techniques that are usable today.
Personally it’s because I don’t enjoy solving the problem once in one language and then transcribing it into a totally different language and worrying I got the transformation correct (+ I still need to write all the same tests).
Isabelle/HOL [1] allows specifying and proving properties about a function/program in Isabelle/HOL and then generating output in Haskell, OCaml, Scala and SML. Granted, you'd need to learn Isabelle/HOL, but you wouldn't need to worry about the transformation process.
Also, afaik proof languages don’t have libraries for building up more and more proofs, and, even if they did, they’re not going to come bundled with random runtime dependency X I picked to implement it.
The Archive of Formal Proofs [2] is a collection of Isabelle theories (proof modules) that you can easily integrate into your own proofs. Some proofs in the AFP are about specific properties so they're not that interesting as a proof library, but many others include reusable specifications that are useful in other proofs.
I'm not quite sure about the runtime dependency aspect you mention. In general, proofs about data structures and algorithms are interesting, but proofs about glue code or I/O interfaces are mostly useless and a waste of time (depending on the context). For example, proving your sorting algorithm is correct is a good fit for formal verification, but proving your network code uses the correct flags in a socket creation syscall is hardly interesting and provable.
I'm only familiar with Isabelle/HOL, so my comment is limited to that environment.
I didn't mean to disparage your post nor did I intend to come across as angry if that's how it landed (sorry). You just asked the question of "why isn't this done more often" & I was adding my perspective.
Isabelle/HOL [1] allows specifying and proving properties about a function/program in Isabelle/HOL and then generating output in Haskell, OCaml, Scala and SML. Granted, you'd need to learn Isabelle/HOL, but you wouldn't need to worry about the transformation process.
These languages are not the most commonly ones used in the industry (Java, C#, JavaScript/TypeScript, C/C++, Rust, Python etc). I'm particularly interested in C++ and JavaScript/TypeScript if you know of any.
I'm not quite sure about the runtime dependency aspect you mention. In general, proofs about data structures and algorithms are interesting, but proofs about glue code or I/O interfaces are mostly useless and a waste of time (depending on the context). For example, proving your sorting algorithm is correct is a good fit for formal verification, but proving your network code uses the correct flags in a socket creation syscall is hardly interesting and provable.
What I was saying is that you may have a distributed system that makes up multiple components. Usually each component individually is already pretty hardened. The errors indeed pop up in the glue code where you're sending messages between those distributed components. Less so about the correct flags in socket creation but "did you remember to handle error case X?", "did you manage the state transitions correctly for distributed messages?", "is the custom caching layer I layered on top of the distributed component interacting correctly with that component?", "did I correctly implement 2PC?", etc. For example, imagine that you used YuggabyteDB. YuggabyteDB may have proofs around its behavior. However, if I want to write a proof for my usage of it, I'm going to have to pick generic components that describe a "distributed database" and customize what kind of isolation level I'm expecting between transactions. Some of this can be expressed generically and maybe there are such components already written. Some of the stuff those is extremely nuanced like "DB X implements operation Y in a nuanced way".
I'm not saying these are all necessary for the purposes of getting value out of type checking. I am suggesting that the difficulty for type checkers to be used in that way, the lack of proof "APIs" for components, the challenge of dictating runtime language auto generation / manually translating is a reason you haven't seen a massive rush towards formal proofs I think.
Comments
Before I begin - I hope my comment doesn't come across as too confrontational. I don't want to invalidate your experience, but I'd like to spread information about formal verification techniques that are usable today.
Isabelle/HOL [1] allows specifying and proving properties about a function/program in Isabelle/HOL and then generating output in Haskell, OCaml, Scala and SML. Granted, you'd need to learn Isabelle/HOL, but you wouldn't need to worry about the transformation process.
The Archive of Formal Proofs [2] is a collection of Isabelle theories (proof modules) that you can easily integrate into your own proofs. Some proofs in the AFP are about specific properties so they're not that interesting as a proof library, but many others include reusable specifications that are useful in other proofs.
I'm not quite sure about the runtime dependency aspect you mention. In general, proofs about data structures and algorithms are interesting, but proofs about glue code or I/O interfaces are mostly useless and a waste of time (depending on the context). For example, proving your sorting algorithm is correct is a good fit for formal verification, but proving your network code uses the correct flags in a socket creation syscall is hardly interesting and provable.
I'm only familiar with Isabelle/HOL, so my comment is limited to that environment.
[1] https://isabelle.in.tum.de/overview.html
[2] https://www.isa-afp.org/
I didn't mean to disparage your post nor did I intend to come across as angry if that's how it landed (sorry). You just asked the question of "why isn't this done more often" & I was adding my perspective.
These languages are not the most commonly ones used in the industry (Java, C#, JavaScript/TypeScript, C/C++, Rust, Python etc). I'm particularly interested in C++ and JavaScript/TypeScript if you know of any.
What I was saying is that you may have a distributed system that makes up multiple components. Usually each component individually is already pretty hardened. The errors indeed pop up in the glue code where you're sending messages between those distributed components. Less so about the correct flags in socket creation but "did you remember to handle error case X?", "did you manage the state transitions correctly for distributed messages?", "is the custom caching layer I layered on top of the distributed component interacting correctly with that component?", "did I correctly implement 2PC?", etc. For example, imagine that you used YuggabyteDB. YuggabyteDB may have proofs around its behavior. However, if I want to write a proof for my usage of it, I'm going to have to pick generic components that describe a "distributed database" and customize what kind of isolation level I'm expecting between transactions. Some of this can be expressed generically and maybe there are such components already written. Some of the stuff those is extremely nuanced like "DB X implements operation Y in a nuanced way".
I'm not saying these are all necessary for the purposes of getting value out of type checking. I am suggesting that the difficulty for type checkers to be used in that way, the lack of proof "APIs" for components, the challenge of dictating runtime language auto generation / manually translating is a reason you haven't seen a massive rush towards formal proofs I think.