News for hackers. Stuff that matters.

A comment on AMD ships microcode update to disable some branch prediction. Parent comment

Re:AMD ships microcode update to disable some branch prediction by pkaye on Friday January 05, 2018 @06:25PM (#16082679)
What happened to all the theorem proving software that are supposed to absolutely guarantee correctness of code. I guess they are only as accurate as the assumptions input into them?
[ Parent | on HN ]
Re:AMD ships microcode update to disable some branch prediction by zlynx on Friday January 05, 2018 @06:59PM (#16082847)
In this case the CPU does function exactly as designed. Any correctness prover would agree.

It does show the problem of all theorem provers: they are only as good as the specification.

[ Parent | on HN ]
Re:AMD ships microcode update to disable some branch prediction by SAI_Peregrinus on Saturday January 06, 2018 @09:14AM (#16085320)
The code conforms to the specification. It's not buggy.

The specification does not conform to the user's expectations or documentation. It's flawed.

Theorem provers can only prove that the code conforms to the specification, not to the user's expectations or documentation. They can be very helpful, but they aren't magic and can't interpret non-formal specifications.

[ Parent | on HN ]