Hacker News Reader

Killbits is the one I've heard most commonly - as the talk says, most modern processors have a bunch because it's impossible to test every possible edge case a priori.

(Good recent examples include the AMD lockup bug that Matt Dillon found, and the nasty counter-example of the Intel Quark segfault bug, which can't be worked around so easily because the Quark doesn't have killbits. "Oops.")

View on HN

>most modern processors have a bunch because it's impossible to test every possible edge case a priori.

Only with the sort of engineering most current CPU manufacturers use.

It's possible to have formally verified hardware; it's just expensive with current tech. Tools are improving, though. I suspect the next cutting edge will be the unification of functional-language-to-hardware compilers like Clash or Lambda-CCC with fully dependent languages like Agda or Idris, where you can statically verify arbitrary properties though the type system.

I've just written an Idris programm that determined "your mothers phone number", hows that for arbitrary facts? (tip of the hat to xkcd.)

Reply on news.ycombinator.com