upvote

points

by jongjong5 hours ago |
comments
upvoteby gr_norm5 hours ago|
next
[-]
> How to prove the correctness of the mathematical specification?

You can show that your specifications satisfy well-accepted criteria like confidentiality and integrity. This is usually done as the final verification step. For example, AWS just did it for the Nitro hypervisor used by EC2: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng....

reply
upvoteby stevenhuang4 hours ago|
prev|
next
[-]
So it moves from both "my implementation and specification is incorrect", to just "my specification is incorrect".

I don't understand this type of thinking. Proving what you can is still better. Don't let perfect be the enemy of good.

reply
upvoteby jongjong2 hours ago|
parent|
[-]
>> Don't let perfect be the enemy of good.

I feel like the exact same line could be used to argue the opposite point against formal verification.

I'm not saying that proof is inherently bad. If it was free, then I agree it would be good, but my point is that it's not free. Proofs are expensive to produce, maintain, they lock-down flawed implementations, focus on correctness but disregard more important aspects like modularity (I.e. loose coupling, high cohesion). Also; formal proofs discourage change and they create false confidence about reliability because sometimes the bug is in the spec itself, especially as the spec gets more complicated.

I think modularity is a more useful property to aim for in terms of achieving the right degree of correctness over the life of the software, in a practical sense.

Formal proofs can work against modularity if the proof must be rewritten in order to achieve modularity as requirements change over time; which is the reality for most software.

reply
upvoteby atoav41 minutes ago|
prev|
next
[-]
That means when one goes out of whack, someone will notice. E.g. let's say the mathematical property is correct, but someone optimizes some behavior. Without tests or verification that could break production or worse: not break it, but break security without anybody noticing.

That is worth the hassle for some applications.

reply
upvoteby lou130627 minutes ago|
prev|
[-]
> people who aren't able to write correct code are somehow able to write correct mathematical specifications

This describes about one or two thirds of the Theoretical CS academic community (conservative estimate) /s

> This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself

I find this hard to believe. The mathematical specification for "array a is sorted" is "forall n in Nat: 0 < n < len(a) -> a[n] >= a[n+1]". The average sorting algorithm is usually a tad longer than this.

> the mathematical spec would get completely invalidated every week or so each time you did an update

Well of course nobody serious advocates for formalizing/verifying code that is subject to that much churn (be it internal or external).

reply