Re:Testing a Formally Verified Compiler
by wtroughton on Monday May 22, 2023 @01:03AM
(#36027658)
A compiler is a theorem prover, sure, but compilers vary in terms of expressiveness of the propositions it is capable of proving (a Python interpreter would be a very weak theorem prover ;) )
Consider: is there an equivalent concept of Turing Completeness for compilers with respect to computational propositions?
Re:Testing a Formally Verified Compiler
by DonaldPShimoda on Monday May 22, 2023 @09:17AM
(#36031051)
I know what you're saying, but there's a difference between "the expected behavior has been rendered as a proposition" (what I said) and "the expected behavior corresponds with a proposition" (what you're saying).
To "render something as a proposition" means for it to be literally written down in the terms of formal logic. Writing a program in Python doesn't generally constitute this form of expression, but writing a proof of a Python program would.
All programs that don't contain undefined behavior satisfy this (in an annoying tautological way) because all programs are proofs of themselves. So the thing you're getting paid for, if you are, is to ask the right questions of your theorem prover (which may be a Python interpreter).