Last but not least, those deciders were implemented and verified in the Rocq pro... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		ufo 5 months ago \| parent \| context \| favorite \| on: Determination of the fifth Busy Beaver value Last but not least, those deciders were implemented and verified in the Rocq proof assistant, so we know they are correct.

lairv 5 months ago [–]

We know that they correctly implement their specification*

meithecatte 5 months ago | [–]

No, they are correct, because the deciders themselves are just a cog in the proof of the overall theorem. The specification of the deciders is not part of the TCB, so to speak.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact