6 ms·
Doesn't that rely on, often incorrect, assumptions of underlying hardware? Doesn't this change based on the environment that the system is going to be put in? T
by gravypod 10y ago
Doesn't that rely on, often incorrect, assumptions of underlying hardware? Doesn't this change based on the environment that the system is going to be put in? There are things people are saying are "guaranteed" about formal systems that just aren't true.
To have a formal system actually be "correct" it needs to have never touched "incorrect" software or hardware. This contains, but is not limited to, a "correct" compiler and hardware implementation.
This is, I'd say, often not the case.
- vilhelm_s 10y agoRight, whenever you try to use mathematics/logic to reason about the real world, you risk that some of your assumptions may be wrong. Every formally verified project will have some set of trusted assumptions. But hopefully this can still dramatically reduce software vulnerabilities---for example, systems more often fail because of bugs in the program logic than bugs in the x86 processor, so assuming a specification for the hardware and proving the program correct with respect to that should still be helpful. (As an aside, hardware and compilers are actually comparatively tractable things to verify--the specifications are well-defined, and they are used by lots of clients so the effort to verify them pays off better. I think in the future, we are more likely to have unproven application programs running on top of proven compilers & hardware than the opposite.)