Dacit · HackerTrans

8 часов назадdiscuss

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...

Dacit

7 дней назадdiscuss

>(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).

Dacit

5 месяцев назадdiscuss

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.

Dacit

5 месяцев назадdiscuss

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.

Dacit

5 месяцев назадdiscuss

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...

Dacit

5 месяцев назадdiscuss

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...

comments