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