Torturing Rustc by Emulating HKTs
harudagondi.spaceI've been playing around with type mapping like this in a highly experimental crate. The ability to map, filter and reduce types is insanely powerful but it's tough to get ergonomic syntax.
I also hit a funny compiler end-of-the road last month when I wanted to try out generic_const_exprs for my RFC8366 implementation:
pub struct VoucherDetails<C>
where
C: CapacityConfig,
[(); C::SERIAL_NUMBER_MAX]:,
[(); C::MANUFACTURER_PRIVATE_MAX]:,
[(); C::IDEVID_ISSUER_MAX]:,
// <imagine a dozen more properties here>
[(); C::NONCE_B64_MAX]:,
{ ... }
Nice.
You inspired me to look up RFC8366. That's a remarkable document, apparently written in English, where at least the abstract and introduction look like they might be the result of a particularly nerdy game of Mad-Libs. :)
I, personally, have never observed a pledge doing anything other than being heard, although I observed Lemon Pledge smelling unpleasant. But, in RFC8366, pledges can join domains!
(I assume that a manufacturer makes a device and the device somehow contains a "pledge" from the manufacturer that the device is what it says it is...)
You assume almost correct, the device is the pledge itself! RFC8366 is used (among others) in the BRSKI protocol family. For device attestation purposes in 802.1x Networks, a pledge comes with a manufacturer provided public key material, often a certificate but not always, that links it to the manufacturer via a publicly available trust root. In an exchange process, the customer - called the registrar in the specification documents - then asks for and verifies the pledge's key material before issuing their own domain certificates.
It's in essence an automated zero-trust-ish protocol for network join purposes :)
This was incredible, even as it rapidly outpaced my PL and mathematics knowledge.
Like I said to a friend, I know just enough category theory to know that I do not understand. Perhaps upon Nth reading.
I think I'll just point to this post the next time some asks me what getting nerdsniped means.