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.
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.