4 ms·

I don't understand this. In order to use formal verification you have to provide a complete and correct specification of what you want the software to do. We a

• danpalmer 10y ago
  Programming languages range in their formality. At the low end you have things like Python or Ruby, where you can write a loop over a type that can't be iterated, and it will crash at that line of code. In the middle you have languages like Java, C#, at the mid-high end, even Haskell and F#. In these languages they enforce type safety at varying levels throughout the code, by first inferring the types at each point throughout the code, and then seeing whether they are consistent. You would not be able to loop over a non-iterable object here. At the really high end you get into the realm of languages like Idris, Agda, and Ivory, and "formal verification" techniques. At this level you can not just write a loop, but you can write a loop that it is possible to prove terminates regardless of the input to the loop. This is done by setting constraints, and proving those constraints all the way through the code - the compiler will infer a lot of this, but it is still more work. This is a very simplified view of it, but essentially the more formal you get in the specification, the less chance that the program can do something unintentional, crash, or be hacked. The vast majority of the code written today is not that formally specified.
• fmap 10y ago
  Programming languages have to be (efficiently) executable, specifications can be logical/declarative. E.g. in a specification I can state things like "forall functions, with uncomputable property foo, we have bar". Plenty of things are uncomputable (e.g. quantifiers over natural numbers), but useful in specifications. There are good and bad specifications, same as for programs. For the semantics of a programming language you could essentially transcribe an interpreter in the form of a structural operational semantics and these are relatively error prone. Instead, you could give an axiomatic semantics, which is a lot more high-level. An equivalence proof between the two gives you a high level of assurance that the operational interpretation you had in mind while writing your interpreter actually means what you think it means. A recent example, the formal specification of the weak memory model of C11 turned out to be wrong (in the sense that it forbids common compiler optimizations, because programs have access to a time machine), but this was discovered when trying to develop a program logic for C11. In practice, most broken specifications I have seen were written by people who never really worked in formal verification. I am not aware of a single instance where a piece of formally verified code was broken because of a broken specification. There are cases where the specification had to be extended. E.g. CompCert was initially developed as a whole program compiler and the spec had to be extended for separate compilation. This broke the alias analysis.