You're viewing the discuss.systems public feed.

Federated feed Local feed

abadidea0xabad1dea@infosec.exchange
Jul 29, 2026, 10:08 AM
@mario @shelldozer it very well may be the most formally correct piece of software we've ever produced, but keep in mind it still has to run on a physical computer it's sharing with less-verified software and is also vulnerable to things like Rowhammer-class ram corruption attacks if one wants to intentionally manipulate it.
There's no final escape hatch beyond which a computer can be absolutely guaranteed to always compute the correct answer, especially when someone has a vested interest in getting it to output the wrong answer.
💬 2🔄 1⭐ 13

Replies

Mariomario@don.tbully.me
Jul 29, 2026, 10:10 AM
@0xabad1dea @shelldozer ~but that's not a bug anymore, that is a hardware issue. my scope was correct software.~
i'm tired, sorry :ablobcatmelt:
i believe there is a way to archive perfect software, be it in a very limited environment.
💬 0🔄 0⭐ 0
calx u-latorcalx@infosec.exchange
Jul 29, 2026, 11:01 AM
@mario @0xabad1dea @shelldozer right, that's not a bug in software
so, you can say the following isn't true for metarocq
> Theorem provers aren't magic, and have bugs just like all other programs.
but having the probability of hardware issues still makes the following true
> Theorem provers aren't magic
💬 1🔄 0⭐ 1
calx u-latorcalx@infosec.exchange
Jul 29, 2026, 11:04 AM
@mario @0xabad1dea @shelldozer not to say, they aren't magic, like i love theorem provers, and they are in a way very magical pieces of software humans have come up with
all this means is they shouldn't become the single source of truth
💬 1🔄 1⭐ 4
Mariomario@don.tbully.me
Jul 29, 2026, 11:09 AM
@calx @0xabad1dea @shelldozer but they actually aren't magic :blobcat3c:
especially isabelle and rocq are actually somewhat easy to break down to their theoretic basics. they are very good tools to learn about proof theory.
💬 2🔄 0⭐ 0
Mans Rmansr@society.oftrolls.com
Jul 29, 2026, 11:17 AM
@mario @0xabad1dea @calx @shelldozer Even with a flawless theorem prover, it is possible that what was proved isn't what you think it is because you made a mistake when formalising the theorem.
💬 0🔄 2⭐ 7
Mariomario@don.tbully.me
Jul 29, 2026, 11:22 AM
@mansr @0xabad1dea @calx @shelldozer but that's out of scope of a theorem prover. that's on the person doing the formalization.
💬 1🔄 0⭐ 0
Crazazy @ my computer c:crazazy@tiny.tilde.website
Jul 29, 2026, 5:15 PM
@mario @0xabad1dea @calx @shelldozer @mansr if the person in question is formalizing a theorem prover, then that's definitely in the scope of problems.
Also you run into some gödel-esque problems when trying to fully prove the consistency of a theorem prover, within the theorem prover itself, so there are probably _some_ limits
💬 1🔄 0⭐ 3
Mariomario@don.tbully.me
Jul 29, 2026, 5:20 PM
@crazazy @0xabad1dea @calx @shelldozer @mansr
> limits
depends on the logic at hand. like first-order logic is complete and afaik solved within less than 200 characters of prolog
peano is incomplete, but here are other arithmetics that are complete like presburger that is complete.
💬 0🔄 0⭐ 0
calx u-latorcalx@infosec.exchange
Jul 29, 2026, 11:19 AM
@mario @0xabad1dea @shelldozer ooo, interesting
tho, i'll have to read about them and metarocq before i can comment
💬 0🔄 0⭐ 1
Haelwenn /элвэн/ :triskell:lanodan@queer.hacktivis.me
Jul 31, 2026, 7:30 PM
@0xabad1dea @mario @shelldozer Yeah, although couldn't that be minimised a lot by running the checks on different kinds of hardware and underlying implementations? (Given portable enough code)

Also coming from a more "trusting trust" point-of-view, quite glad they note that proving Coq in Coq itself has quite few problems.
💬 0🔄 0⭐ 0