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