I think one reason for the web interface is that the device stays usable. If it would export a block device then it would need to unmount the file system on itself or at least block changes. If I remember correctly in the old days before MTP, all Android did this, making storage on the device itself unavailable while making it available via USB.
Yeah, that would be an issue with presenting the device as a block storage device.
The web interface also has a couple of other advantages: the tablet simultaneously listens for ssh connections, and can be used over Wi-Fi, IIRC? Though it could also expose a "USB HUB" with both the network interface and block storage.
I just wish we had a more ubiquitous "network file storage" protocol. The tablet itself could offer NFS, but mounting it under different operating systems would be a pain, requiring manual user intervention.
The trick is that the human only needs to read and understand the Lean statement of a theorem and agree that it (with all involved definitions) indeed represents the original mathematical statement, but not the proof. Because that the proof is indeed proving the statement is what Lean checks. We do not need to trust the LLM in any way.
So would I accept a proof made by GPT or whatever? Yes. But not a (re)definition.
The analogy for programming is that if someone manages to write a function with a certain input and output types, and the compiler accepts it, then we do know that indeed someone managed to write a function of that type. Of course we have no idea about the behaviour, but statements/theorems are types, not values :-)
The thing is, when AI systems are able to translate intuitive natural language proofs into formal Lean code, they will also be used to translate intuitive concepts into formal Lean definitions. And then we can't be sure whether those definitions actually define the concepts they are named after.
Once more I an happy to use the ESR version of Firefox where stuff like this tends to only land much later. Add on top of that the Debian patches and default settings and it's a fine user-agent again :-)
Edit: oops, looks like 115 is the next ESR version, does that mean it gets this "feature" but for a long time will not get proper UI go control it? :-(
Good point, but I think the feature that I can paste any fediverse URL into the search field on my own mastodon instance and view it there, solves around 40% of the problem.
There are also already browser extensions which automatically redirect you to your own instance I think, but those need access to all browsing :-/
Nice example, which opened a small rabbit hole for me: what does "first occurrence wins" mean for options that are meant to be used multiple times, such as "Port" in sshd_config. The man page only says "Multiple options of this type are permitted.", but now I wonder what happens when I put my own Port into /etc/ssh/sshd_config.d/whatever.conf but leave "Port 22" in sshd_config? Or is the (new since bookworm) default sshd_config commenting it out for this reason?
More generally, for multi-options do we maybe want "first file wins"?
Reading in general to more specific configuration directories in order and using the last value read makes the most sense to me. This is usually how I write my own applications.
Anyway, I thoroughly document the order and precedence, but the suggestion from Chris' blog to report more detail about the process is a good one.
