Good luck formally proving Linux. | Hacker News

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

		thfuran on March 17, 2024 \| parent \| context \| favorite \| on: LLM4Decompile: Decompiling Binary Code with LLM Good luck formally proving Linux.

layer8 on March 17, 2024 [–]

The goal is to prove that the source code matches the machine code, not to prove that the code implements some intended higher-level semantics. This has nothing to do with formally proving the correctness of the Linux kernel.

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