4 ms·

This is all exciting and relevant progress, but the technique does not seem to converge towards a real solution in the long run. We developed higher-level lang

This is all exciting and relevant progress, but the technique does not seem to converge towards a real solution in the long run. We developed higher-level languages like C to specify and generate machine code easier and with less errors. Then it turned out with the higher level language it's easy to make mistakes, too, so let's put another layer of specification language on top to avoid that (e.g. let's do Java). Eventually it will turn out that it's not easy to avoid mistakes in that language as well, so we put another layer on top, and again and again. The gist is that computation is not an easy task and we can't avoid the halting problem, but still it is very good to have tools available that make negotiating through bug space easier.

YeGoblynQueenne 5y ago
>> Eventually it will turn out that it's not easy to avoid mistakes in that language as well, so we put another layer on top, and again and again. That is a risk: if the specification is the entire program written in the specification language, then the same opportunities to make mistakes present themselves when writing the specification, as when writing the program by hand. In this case though the specification language has the advantage of being purely declarative: it's only a statement of pre- and post-conditions without any assumptions about implementation. Such a specification leaves little room for mistakes.
- amw-zero 5y ago
  Are you aware that a huge percentage of accepted math proofs have errors in them? https://lamport.azurewebsites.net/tla/proof-statistics.html https://lamport.azurewebsites.net/tla/proof-statistics.html. The worm at the core of all formal verification is that we mistakenly believe that a result is absolutely correct because formal logic was employed. Logic can be subtly wrong, even though the argument appears correct. The very act of using logic does not imply actual correctness. This is not a dismissal of the field - just a warning. There are many mistakes that can still be made when formally specifying and verifying. To believe otherwise is pure hubris.
  - YeGoblynQueenne 5y ago
    Sorry for not replying. I don't feel comfortable replying to comments that begin with turns of phrase like "are you aware", as in your comment or "do you realise" etc. I find this style of conversation coercive and adversarial and it puts my back up, and I don't want to have internet conversations where I'm made to feel that way.

YeGoblynQueenne 5y ago

>> Eventually it will turn out that it's not easy to avoid mistakes in that language as well, so we put another layer on top, and again and again. That is a risk: if the specification is the entire program written in the specification language, then the same opportunities to make mistakes present themselves when writing the specification, as when writing the program by hand. In this case though the specification language has the advantage of being purely declarative: it's only a statement of pre- and post-conditions without any assumptions about implementation. Such a specification leaves little room for mistakes.

amw-zero 5y ago
Are you aware that a huge percentage of accepted math proofs have errors in them? https://lamport.azurewebsites.net/tla/proof-statistics.html https://lamport.azurewebsites.net/tla/proof-statistics.html. The worm at the core of all formal verification is that we mistakenly believe that a result is absolutely correct because formal logic was employed. Logic can be subtly wrong, even though the argument appears correct. The very act of using logic does not imply actual correctness. This is not a dismissal of the field - just a warning. There are many mistakes that can still be made when formally specifying and verifying. To believe otherwise is pure hubris.
- YeGoblynQueenne 5y ago
  Sorry for not replying. I don't feel comfortable replying to comments that begin with turns of phrase like "are you aware", as in your comment or "do you realise" etc. I find this style of conversation coercive and adversarial and it puts my back up, and I don't want to have internet conversations where I'm made to feel that way.