1) Your model of the world corresponds to the world in which the program runs - for example, hardware is usually assumed to be bug-free.
2) The properties you've proven the program to hold are sufficient to stop the hacker from accomplishing their goals.
3) No bugs exist in your theorem prover.
Seems to me that at some point we want theorem provers to be self hosting, as it were.
That of course won't fix problems with bugs in hardware, and hardware that behaves like analog devices (rowhammer, cold boot, data recovery, stray gamma rays...)
It would obviously help reduce errors but it wouldn't categorically eliminate them.
Particularly, he proved that it is impossible for a formal system to prove its own consistency.
In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes.
This will, however, not protect against deeper issues that are common to all N provers. e.g. Potential biases or mistaken assumptions in the formal verification comunity.
At the end of the day, it is an engineering decision. How much of the available resources are you willing to through at the practical problem of making your implementation approach asymptotically to the theoretical limits. The fact that those limits is indeed a peg or two below perfection is an independent issue.
I strongly advise that to deal with both mistakes and subversion. Mutually-suspicious parties in various countries using different logics, compilers, hardware, etc. with a common, executable spec that's basically state machines or functions. That way they get same output from same input.
So, when I saw Milawa was verified first-order, I immediately looked for other verifications of first-order provers (found 1). Then the idea would be diverse implementations of executable parts of that stack with diverse reviews of logic combinations they did. Exhaustive testing done by each party. Even do implementations of key parts of TCB in other logics to check results. The prover with its code is trustworthy when everyone got the same results on same logics, code, shared tests, and individual tests. Plus have paper copies of the resulting text files with hashes stashed away somewhere in case a nation-state wants to throw money at countering diversity via hacking host systems. ;)
Then we rinse and repeat for more complex provers. The fun never stops in this game.
In practice, even much simpler theorems would already raise our confidence a lot. E.g., the inference rules of Coq can be stated in a couple of pages of text, but the kernel checker that you need to trust is 14k lines of OCaml. A proof that the checker actually correctly implements the inference rules would already catch the majority of the bugs that happen in practice. Because of Gödel we then can't hope for a proof in Coq that there is no way to use those inference rules to derive False, but that's less of a concern.
This seems like the perfect time to misquote Groucho Marx: "This is so simple a child of 5 could prove it. Somebody bring me a child of 5!"
Assuming that the computer programs under study aren't allowed to interact with a disk, of course. :-)
Not one that can handle Peano arithmetic—but there are plenty of interesting systems sub-Peano arithmetic. Presburger arithmetic (https://en.wikipedia.org/wiki/Presburger_arithmetic) is the one that springs to mind; I doubt that it's directly useful as a theorem prover, but it does show that interesting mathematics can be done in complete theories.
On the other hand, a theorem prover does not have to be able to prove everything about a system to be able to prove some useful things. One might also say "the system mathematicians are interested in is all of mathematics, which is more powerful than arithmetic", or, for that matter, "the system programmers are interested in is all of theoretical computation, which is (at least) Turing complete"—but sometimes it's useful intentionally to restrict our power. (I think of https://news.ycombinator.com/item?id=10567408 , for example.)
(If we're being very picky, then, as pfortuny points out (https://news.ycombinator.com/item?id=12762192), a computer, having only a finite address space, isn't even as powerful as ordinary arithmetic; but it's fair to guess that this isn't a useful kind of pickiness.)
To put it another way, in order to disqualify self-reference, you would need to employ a higher order proof system--which gives the game away anyway.
This is a good not-too-technical but not-condescending explanation https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081... (it does get into the technical details; it just doesn't go line by line as you would if you wanted to recreate the proofs).
As long as you have the expressive power of Peano arithmetic (which all programming languages ought to, and definitely all proof systems ought to), you can find a Gödel sentence in the system and thus prove that it can't prove, of itself, "x is consistent".
It's worth looking into, if only for the enjoyment.
You do know that Shannon proved that general purpose compression is impossible, right? Why bother if that 75% compression ratio is provably impossible?
Even if Gödel is shown to apply in the strict generalized theoretical sense, it might be irrelevant to practice. Theory and practice often differ enough for practice to be very useful; we easily prove halting for most programs we care about, compute solutions to average-case NP-Complete problems without a noticeable rise in CPU temp, and (as the other poster at this level said) write compression algorithms which work well on all relevant inputs. This is poor analogous reasoning, of course, but I include it because demonstration of universal practical pitfall would be very interesting in much the same way specific manifestations of availability loss in fault-tolerant consensus algorithms are interesting.
Really though, I am tired of the above exact exchange playing out in every thread I've seen here on formal verification. Someone raises the obvious concern of bugs in the theorem prover. Someone else raises the bootstrapping solution, cribbed from compilers. Someone else raises the Gödel objection; and there the conversation dies. Dig deeper.
My favorite counter to the Godel thing, esp about termination, was sklogic showing how far from reality these concerns were by illustrating that a while loop counting down toward zero with "stop if zero" condition will guarantee a termination of any algorithm working piece-by-piece in inner loop so long as hardware functions. No magic math at all required to defeat the termination requirement in real-world. I added watchdog timers or even shelf-life of modern parts can do the same.
I did something similar when I was concerned about infinite loops or DOS attacks from malicious input. Just box it up in something I know will work with something checking up on it. Another was algorithm theory telling me QuickSort performed better but choose HeapSort if worst-case is a problem. A smarter programmer told me to just time average for QuickSort, run it with a watchdog, kill it on any instance it takes too long, and use HeapSort for that instance. Those are the kind of tips I appreciate about these terrible problems the theoretical side brings me. Hell, if only theory people would find, generalize, and expand on all the effective cheats in engineering instead of idealistic or abstract stuff. :)
Plus, hardly anyone is making a self-verifying prover. Someone just asked about that. I tried what I hope is the proper response of simply linking to a self-verifying prover that succeeded in that goal up to first-order logic. So, that's already done with us just needing similar ones for checkers of HOL, Coq, ACL2, etc. Contrary to your implication, the Milawa techniques are based on and supporting some of most practical verification work to ever be done. So, one of few times someone totally ignored Godel in what non-experts would consider Godel's domain led to one of best results in formal methods.
We don't need Godel at all in these discussions. We just need to explain what formal methods are, their successes, their limitations, how to properly use them, and ideas for new projects.
Notice though, Gödel's incompleteness didn't end formal logic (all the better for Gödel). I know we're in a public forum, but I would note that your "But what about the practical applications!?" is misplaced (though not poor analogous reasoning--I think you're hitting the nail on the head, honestly). Formal verification is not futile because of Gödel's proof. However, a self-verifying formal system is--which is a useful insight, especially for those interested in formal verification.
As an aside, I don't think you need to convince anyone that's actually recreated Gödel's proofs to approve of continued work on formally verified code. We would get excited about that stuff even if it weren't practical.
On page 12 of the english translation (and possibly the original german), Godel addresses certain criteria for distinguishing a sufficiently powerful system (as well as recursively axiomitizable, etc).
I have personally written such a software verification scheme, and even have an inferior interaction mode for SMT solvers that can help you verify such schemes (it's in my profile & github).
There are also great books like the extremely cheesily-named graduate textbook: "Your Guide to Automated Reasoning", that examine this issue from every perspective imaginable.
https://www.cs.utexas.edu/~jared/milawa/Web/
They and their associates' work covers verified runtimes, HOL, extraction mechanisms, etc.
https://www.cl.cam.ac.uk/~mom22/research.html
Just port Milawa to run on multiple architectures with separate CPU's or implementations from multiple vendors. Include verified, VAMP processor on two FPGA's. Check Milawa itself then check the software in FOL until HOL is done. I have a paper somewhere on HOL-to-FOL converter, too. :)
Note: I've seen a bunch of things implemented in Prolog. I figure it could be modified to execute the program and produce an execution trace of its logic that could be run through Milawa. Not specialist enough to say. A prior, certified compiler for Pascal-like language was specified in Z shown equivalent to Prolog functions. So, there's potential here.
This is not to say that self-hosting isn't useful, since most bugs are not likely to be of this form.
I feel like exploits like Rowhammer really threw a wrench into this. Now one would also have to specify allowable interactions with the hardware?
Thought experiment; you are some sort of intrusion prevention system. You've detected that your hardware is untrustworthy. Now what?
Now, the analog and RF portions are The Devil. These will be a (censored) to get correct with automated means. Already are with manual methods. There's been some progress in synthesizing and verifying them. Still mostly ad-hoc, manual work. Best bet is analog portions... much as one can use... happen with simple components on as old a process node as you can use. Less design rules, less weird physics, more reliability due to maturity of processes, and more synthesis results. Either whole thing is done on old nodes or we can pull a Tekmos doing old (eg 350nm) for analog with new (eg 90nm) for digital part with careful integration.
EDIT: To address other commenter, put it behind EMSEC shielding to address that. The analog components can also be designed for fault-tolerance against things like cosmic rays or voting configuration used to correct errors.
Hamilton's 001 Tool Suite http://htius.com/
Cleanroom Software Methodology http://infohost.nmt.edu/~al/cseet-paper.html
Praxis Correct-by-Construction http://www.anthonyhall.org/c_by_c_secure_system.pdf
All three have some upfront time in specification with Praxis doing refinements, too. However, they all knock out tons of debugging and integration problems since errors don't slip in at all. Altran/Praxis charges 50% premium on top of normal contract so the extra labor is probably less than 50% given they're profitable. Cleanroom anecdotes showed the reduced debugging and maintenance issues meant it actually barely cost anything extra in time or money. A few outliers had it saving time.
There's also a number of people and companies that are encoding business logic into specs that they implement with logic programming languages. This eliminates mismatch between business requirements and code with quite a bit of productivity and safety advantages if it works in one's use-case. I haven't evaluated their effectiveness but here's two:
http://www.missioncriticalit.com/technology.html
https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf
As long as I'm well-actuallying, 2) The proven properties establish my own informal goals. If a hacker's goals are also satisfied, well, maybe they want to DDoS the internet but it's Not My Problem.