The dogma that mathematical proofs could, in principle, be turned into logical proofs remains a conjecture; it is not feasible in practice. Existing proof systems are not up to the job; can they be beefed up sufficiently? Research community disconnect!https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ …
-
-
Famous counterexample :)
End of conversation
New conversation -
-
AFAICT they're still fairly hard to use for "real programming", but recent progress has been impressive here too, eg https://project-everest.github.io/ , a fully-verified HTTPS stack.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Even computer system verification runs into some thorny philosophical problems. Formal verification defines a bug as a mismatch between code and specification, but that's not how people actually use the word "bug" in real life (which is more about the human-software interaction)
-
There is also a tendency to change code and specification to make it more formalisable which can result in bugs (in the informal sense) that were caused by formal verification! Embarassing example: a cipher that was broken because of changes that were made to prove its security
End of conversation
New conversation -
-
-
I came here to say that Kevin Buzzard is doing it, but it turns out that that's Kevin Buzzard's blog you linked. So maybe that does prove there's exactly one person doing it. :P
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.