WSL Containers and Hyperlight are two of the available backends for MXC. MXC is not a replacement for them -- it is not an isolation technology itself, it's a unified management API for leveraging other isolation technologies.

You can use the same API to configure and run code in a WSL Container as you would to run them in an LXC container on Linux, or Seatbelt sandbox on MacOS; or in a MicroVM or a Hyperlight VM.

> Those who understand technology to verify arguments already exists can only come to the conclusion we'd be better of with formal verifiers in legal systems.

Those who understand law know that formal verifiers cannot replace a judge, because every facet of law (the writing of it, the interpretation of it, the application of it, and the enforcement of it) has to account for all the vagueries of human existence.

No formal verifier can account for definitions that need to expand as the scope of human endeavor expands. No formal verifier can determine mens rea. No formal verifier can determine if something is obscene. No formal verifier can determine someone's mental competence. No formal verifier can cover all mitigating factors. No formal verifier can apply mercy where mercy is needed.

> Those who understand law know that formal verifiers cannot replace a judge, because every facet of law (the writing of it, the interpretation of it, the application of it, and the enforcement of it) has to account for all the vagueries of human existence.

Not the vagueries of human existence, only vagueries of law specified in natural language.

> No formal verifier can account for definitions that need to expand as the scope of human endeavor expands.

No formal verifier is expected to account for definitions, the democracy shapes the law, and the law would first need to be rewritten as definitional axioms in the database of axioms, theorems & proofs. The verifier is just a minimalistic algorithm performing substitution maps on sequences of tokens. This is intentionally minimalistic to minimize the error / attack surface on the verifier itself.

(Currently only error hardening has happened for metamath verifiers, so obviously we would want formal proofs of the absence of 0-days in the verifier)

> No formal verifier can determine mens rea.

It's up to the democratic population while formalizing, to either formally define intent (which presumably goes nowhere), or to pragmatically accept that in the absence of external traces of intent the only thing society can do is define action-reaction patterns, not intention-reaction patterns, but again, that's not the formal verifier, but the database of axioms, definitions (and theorems and proof)

> No formal verifier can determine if something is obscene.

The same, if democracy by referring to a concept of "obscene" chooses to place itself in the position of needing to first define "obscene" in the database of axioms and definitions. But no formal verifier needs to determine this, the verifier just checks a proof in a due process fashion.

> No formal verifier can determine someone's mental competence.

The formal (not natural langue) law could specify how to assess mental competence in a secure non-malleable way (if the democracy decides it needs that). I'm not a dictator, it's not up to me to propose the exact definitions. The formal verifier is not the place to handle these issues, those should reside in the database of axioms and definitions.

> No formal verifier can cover all mitigating factors.

> No formal verifier can apply mercy where mercy is needed.

"but the machine will never man-splain like a human could"

"the machine can only mech-splain a bit at best"

Some of the very weakest arguments against formal verification in law. Like being anti due process.

While this discussion is fascinating I think we should scale it back a little. Instead of discussing all aspects I'm quite curious about just one.

How would you define "document" in a way that allows for formal verification? Ideally without relying on words that leave room for interpretation.

You can kinda get close in pure CSS with CSS media queries using the resolution query on dppx measurements; but that only allows you to be as granular as however many distinct "dots per CSS pixel" values you want to add media queries for. Something like this would let you scale by device resolution for both traditional 96dpi screens, higher DPI 192dpi screens, and super high resolution 288dpi screens:

    body { --resolution-scale: 1; }
    @media (min-resolution: 2dppx) { body { --resolution-scale: 2; } }
    @media (min-resolution: 3dppx) { body { --resolution-scale: 3; } }
    .myPixelSizedElement { width: calc(96px * var(--resolution-scale)); }

But unfortunately there's no way to directly use the devicePixelRatio value you can read from Javascript directly in a CSS calculation to be able to get a precise scaling on any arbitrary pixel density.

Much simpler, you also just have JS update (and keep updated - initial DPI is not always the current DPI) --devicePixelRatio under :root on the client side. Something like that existing by default is all that's really missing.