3 ms·
The point is that you're not going to do formal verification of your software. There is actually very little formally verified software out there, and the verif
by Aaargh20318 9y ago
The point is that you're not going to do formal verification of your software. There is actually very little formally verified software out there, and the verified code that does exist is relatively small.
And no, you can't rely on the compiler to get it right. Maybe if you only write Haskell you can get there 99% but there will always be human errors in code that the compiler can't find.
- eru 9y agoWe rely on computers to get parts of our spec right all the time. Yes, a higher level language lets you offload more to the computer (like Haskell), but even in C we are doing some off that. Yes, in practice you seldom have much of a formal spec, agreed.