Even if you write a formal specification the operating system the code runs on is almost certainly not formally specified so you're just moving the trust boundary slightly further out to the OS & associated libraries.

▲

skydhash 2 hours ago | parent [-]

That also assumes that your axioms are correct and the verification code is also correct. It's also a lot of work to update your system, when assumptions are challenged.

	▲	112233 15 minutes ago \| parent \| next [-]
		exactly. somehow many people have the idea that C-like imperative code harbours bugs because it cannot be formally reasoned about, and the answer is writing code that can be formally reasoned about. That the resulting code is many orders of magnitude larger and more complicated than the "informal" original, and often simply cannot exist, and is incomprehensible to most humans if it does, is left as an exercise for the reader. I mean, formal methods cannot even prove collatz conjecture terminates. Somehow that thing seems to be running some sort of almost turing complete machine in the number encoding. Good luck formalizing existing software!
	▲	measurablefunc 2 hours ago \| parent \| prev [-]
		I agree.