Metamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.
The cables are supposed to be labelled with their maximum speed (5, 10, 20, 40, or 80 Gbps or nothing if no data) and maximum wattage (60W or 240W).
HOWEVER, I don't remember ever seeing a cable with such a label. I'm sure they exist, but I don't see them. Requiring products to be labelled, and treating mislabelling as fraud, could mostly solve this. It's definitely a real problem.
> Requiring products to be labelled, and treating mislabelling as fraud, could mostly solve this.
There are too many manufacturers to hunt. Basically USB-IF needs to stop almost all shipments in the world. That's not going to happen.
USB spec is completely open and free to obtain. While it allows people to develop and DIY many things, it also attracts bad manufacturers like flies.
Good certified cables with correct markings exist. There are companies like Cable Matters or Startech who bother to actually certify their cables and get USB-IF TIDs. They do cost you quite a bit money though. Here are some:
In Metamath the proofs hide absolutely nothing. There's no hand-waving "it's obvious that". Every step in a proof must be rigorously and directly proven by some axiom or a previously-proven theorem with absolutely no exceptions. This also means that while finding proofs can be hard, verifying proofs is fast. I just ran a proof verification run of over 47,000 theorems in 6.35 seconds. In the Metamath Proof Explorer / set.mm database (the one with classical logic and ZFC), we routinely run multiple provers by different people on every proposed change. So not only is the kernel small, it's implemented by multiple different programs, making it extremely unlikely we'll accept an invalid proof.
Metamath is interesting for education in the principles of formal proofs, because:
1. The Metamath Book is self-contained well written, simple introduction.
2. Everything is explicit, nothing is hidden.
3. Because of extremely simple syntax and semantics it's easy write own proof verifier.
The drawbacks are:
1. Non-standard approach to free and bound variables.
2. Very weak logic in comparison to Lean. The logical syntax rules and logical semantics rules used for proving mathematical statements in Metamath, have to be explicitly specified in the Metamath database. In Lean they are part of the Lean kernel. An bug in this Metamath specification is equivalent to a bug in Lean kernel.
3. Almost no proof automation. No tactics. Long, hard to read proofs.
I would characterize Metamath as the assembly language of proof assistants, very low level and detailed way to write proofs.
What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://github.com/digama0/HOL
Reading `hol.mm` made me grateful for Lean 4's general purpose programming.
I get the string substitution focus, and respect what metamath has achieved, but the bridge Lean 4 makes wrt systems programming has left quite an impression.
I wonder how many people mostly see mathlib4 & think that's the one prescribed route (ala Rust) when one of Lean 4's under-documented super powers is the ease with which you can roll your own light-weight low to zero overhead domain-specialized constructs that are also trivial to prove because of the dependent type system.
(Perhaps more for verified functional systems than deep math.)
There are other forms of logic? is intuitionistic logic as rigorous? fascinating
edit: the link says it is a weakening. if it is weakened, how can you prove the same stuff? i am a bit confused but i can see how it is useful for smarter people than me!
> if it is weakened, how can you prove the same stuff?
Sometimes, you can't. In particular, so-called "non-constructive" proofs don't work in intuitionistic logic. Some mathematicians like to work in intuitionistic logic: for philosophical reasons, pragmatic technical considerations, or just because they think it's interesting.
This is not entirely true: non-constructive proofs can be fully understood within intuitionistic logic as proofs of negative statements, viz. statements about what isn't constructively true or doesn't constructively exist. From this point of view, intuitionistic logic can be seen as stronger and more powerful than classical logic, because it can endow positive statements (particularly statements about logical disjunctions or existentials) with computational content whenever they have a direct proof.
Classical logic doesn't bother with this; positive and negative statements are completely dual to one another, and this duality is elegant in its own way (as people who are committed to classical logic will readily point out), but one needs linear logic in order to combine it with an awareness of constructive statements.
Intuitionistic logic can prove less than classical logic, but what you gain is that proofs are constructive. Also you can use it to reason about things for which law of excluded middle doesn't hold (typically types).
I love this, and more generally the Triptych Project. We shouldn't need to use JavaScript to work around important limitations in HTML that are widely needed.
Wait a sec. My understanding is that passkeys are public/private keypairs. Public is in server, so even breaking into a server does not reveal the private key.
The big risk with passkeys is storing the passkey where it will be held hostage. Don't store it in most single-ecosystem devices like Apple. Bitwarden can export, and I think 1Password can as well.
That's where the attestation feature comes in. It allows them to force you into a hostage situations by restricting passkey implementation. There's a reason that was part of the spec from the get go but a passkey transfer system wasn't.
reply