Dacit
Joined 9 months ago
Karma
9
Submissions
6
Member since
Feb 4
Recent submissions
Comment · 3 months ago
You will want at least a separate session for the `restricteduser`: E.g. with X11, a process in the same session can do almost anything with your input/output. And most Linux distributions make it really hard to disable external device access for individual users...
Comment · 4 months ago
>(FWIW) Gemini agrees
LLM hallucination: Poly/ML has been in use since at least 1986 (see e.g. Paulsons preliminary user's manual for Isabelle).
Comment · 8 months ago
You are clearly misinformed. According to German law, you can start a UG (limited) with only 1€ + notary cost. Starting a business with personal liability doesn't cost anything.
Comment · 9 months ago
No. The whole point of the LCF approach is that only kernel functions can generate theorems. Usually this is done by having a Thm module with opaque thm type (so its instances can only be generated by this module) and embedding the base rules of your logical calculus as shallow functions into that Thm module. Thus, all thm objects are correct by construction (w.r.t. your calculus), and you only need to check the Thm module to verify this.
Tactics generate thms by calling functions of the Thm module in some fashion.
Comment · 9 months ago
In the described case, this was a simple user error. But you are right nonetheless: To enable the concurrency, the system uses a parallel inference kernel (https://www21.in.tum.de/~wenzelm/papers/parallel-isabelle.pd...). I have heard the anecdote that in the first version, this also allowed one to prove false, by fulfilling a proof promise with a proof that depended recursively on the same promise.
And there are verification tools for verification tools! Isabelle has a verified proof checker that can check whether a given proof is sound: https://www21.in.tum.de/~rosskops/papers/metalogic_pre.pdf The only caveat is that the proof checker itself is verified in Isabelle...
Comment · 9 months ago
Indeed this can simply be checked by a command-line invocation.
But I don't think the student was aware: They would only have seen a purple coloring of the "stuck" part, as shown in the linked example in the blog post. And if one assumes that the system only accepts correct proof steps, it's very easy to miss a small error in a theorem statement...