3 ms·

Formal software verification encompasses a wide set of what we refer to as advanced mathematics. The process of taking some thing you want the code to do, corre

Formal software verification encompasses a wide set of what we refer to as advanced mathematics. The process of taking some thing you want the code to do, correctly abstracting it out into component lemmas, and generating proofs for those lemmas, is itself advanced mathematics. I don't really see a way that this could be simplified.

screcth 2y ago
Formal hardware verification has been much more successful in industry. Are there fundamental differences in the types of problems that they solve? EDA companies have been able to create tools that don't require a PhD in Math to be used effectively. I think that the explanation for such different levels of success is that economic incentives are different. The cost of a hardware bug is much much higher than the cost of the average software bug; this means that hardware companies are willing to spend a lot of money in getting designs right the first time, versus software companies that know they can always make bug fixes in new versions of their products. Additionally, hardware companies are used to paying millions of dollars in software licenses, which is not common in the software world.
- IshKebab 2y ago
  Yeah I agree formal hardware verification is an order of magnitude easier to use. My guess is it's because the problem is so much simpler. No variables, no loops, no recursion, etc.
  - dumbo-octopus 2y ago
    Yes, the challenge in any formal software verification is dealing with unbounded inputs and compute durations, as enabled by recursive programs. If the code under analysis is straight-line non-reentrant basic logical blocks, the verification is quite trivial indeed. This is vaguely the case for hardware verification, though of course there are complexities introduced by the physical nature of the embedding.
  - staunton 2y ago
    > My guess is it's because the problem is so much simpler. No variables, no loops, no recursion, etc. My guess: it's because people actually care about correctness for hardware. It's really expensive to throw out all those fab runs when you notice you messed up...
  - screcth 2y ago
    That would only cover the simplest feed-forward designs: combinational circuits and versions with extra registers added for timing reasons. As soon as you introduce any kind of feedback in your RTL design it's possible to do any kind of computation that SW can do and therefore proving correctness is difficult.
fweimer 2y ago
Is it really that advanced? Do you actually need more logic tools than what was used in the 19th century to formalize real analysis? Things get complicated if you want to put the proofs into the types, but I don't think this is the main approach the industry uses for certifying software for high-integrity applications (in cases there is a requirement for formal verification, which seems to be less and less the case). I don't think it's the mathematics, it's the tools. If the proof is separate and needs to be kept aligned with the specification and implementation manually, that's not really useful except for niche applications. Integrated approaches (like Verus here, or SPARK in the Ada context) should solve the implementation/proof gap, but such tools are not widely available for languages people actually use.

screcth 2y ago

Formal hardware verification has been much more successful in industry. Are there fundamental differences in the types of problems that they solve? EDA companies have been able to create tools that don't require a PhD in Math to be used effectively. I think that the explanation for such different levels of success is that economic incentives are different. The cost of a hardware bug is much much higher than the cost of the average software bug; this means that hardware companies are willing to spend a lot of money in getting designs right the first time, versus software companies that know they can always make bug fixes in new versions of their products. Additionally, hardware companies are used to paying millions of dollars in software licenses, which is not common in the software world.

IshKebab 2y ago
Yeah I agree formal hardware verification is an order of magnitude easier to use. My guess is it's because the problem is so much simpler. No variables, no loops, no recursion, etc.
- dumbo-octopus 2y ago
  Yes, the challenge in any formal software verification is dealing with unbounded inputs and compute durations, as enabled by recursive programs. If the code under analysis is straight-line non-reentrant basic logical blocks, the verification is quite trivial indeed. This is vaguely the case for hardware verification, though of course there are complexities introduced by the physical nature of the embedding.
- staunton 2y ago
  > My guess is it's because the problem is so much simpler. No variables, no loops, no recursion, etc. My guess: it's because people actually care about correctness for hardware. It's really expensive to throw out all those fab runs when you notice you messed up...
- screcth 2y ago
  That would only cover the simplest feed-forward designs: combinational circuits and versions with extra registers added for timing reasons. As soon as you introduce any kind of feedback in your RTL design it's possible to do any kind of computation that SW can do and therefore proving correctness is difficult.

fweimer 2y ago

Is it really that advanced? Do you actually need more logic tools than what was used in the 19th century to formalize real analysis? Things get complicated if you want to put the proofs into the types, but I don't think this is the main approach the industry uses for certifying software for high-integrity applications (in cases there is a requirement for formal verification, which seems to be less and less the case). I don't think it's the mathematics, it's the tools. If the proof is separate and needs to be kept aligned with the specification and implementation manually, that's not really useful except for niche applications. Integrated approaches (like Verus here, or SPARK in the Ada context) should solve the implementation/proof gap, but such tools are not widely available for languages people actually use.