3 ms·
> It doesn't prove that your specification is bug-free & vulnerability-free. There are formal development methodologies where you start with a small set of ver
by nextos 2y ago
> It doesn't prove that your specification is bug-free & vulnerability-free.
There are formal development methodologies where you start with a small set of very simple axioms and you iteratively refine them. Eventually, you end up with code. All steps are formally verified along the way. This addresses your (valid) concerns. For example, many railway software control systems have been developed this way. See e.g. references [1,2] for some more in-depth discussion. Some of these ideas might make a comeback given that code generation is cheap now, but it's quite unreliable.
[1] https://raisetools.github.io https://raisetools.github.io
[2] https://raisetools.github.io/material/documentation/raise-method.pdf https://raisetools.github.io/material/documentation/raise-me...
- IshKebab 2y agoYeah that's fine if you can do it. His point is that most software is not that simple. I work in RISC-V verification and the spec is full of ambiguously worded or easy to misinterpret or just plain unspecified requirements. Even if you formally verify your chip against a formal specification there's a huge gap between the asciidoc ISA manual and that formal specification where bugs can exist. Something like compression is the absolute best case - you have a trivial property that covers everything. Mostly it isn't like that though.