calx u-lator
M-x lisp-hacker
i like anime, movies, vocaloid, drawing, math, linux, security, emacs, common lisp, mechanical pencils, and you ;)
feel free to message me (or feel costly)
let me know, if i am unknowingly being annoying somehow, i will stop (being annoying unknowingly)
"I don't know everything; I only know what i know"
-- Tsubasa Hanekawa
The LEAST Private Operating System Ever Created
@mario@don.tbully.me @0xabad1dea@infosec.exchange @david_chisnall@infosec.exchange
the assumption that verifier isn't faulty that can be proven actually
but to remove that assumption and to prove it, you'll need to add some other assumption, maybe about the hardware you'll use to prove the previous assumption, or maybe the model modelling the system on which the theorem prover will run
in no way can a theorem prover, escape from its dependence on the assumptions about the system it is running on
a normal proof doesn't have any such hidden dependence