Show me code you've published that is used by real people in real systems that follows the philosophy you've espoused here. Otherwise I'm calling shenanigans.

You are unnecessarily combative in this thread. I don't know what about the GP it is that ticks you off but they're making a lot of sense to me and I don't see why you would be loudly demanding published code when you are having a conversation about an abstract device.

If you haven't read my blog on this topic, I suggest you do so before replying further: https://burntsushi.net/unwrap

It should very clearly state my position. And it provides the examples that I previously referenced.

The GP got a link to this blog in the previous HN thread. They dismissed it out-of-hand without engaging with it at all. And tossed in an ad hominem for good measure. So your issue with me specifically here seems completely inappropriate.

I've presented examples. They haven't. They haven't even bothered to engage with the examples I've provided. I want to read code they've written using this philosophy so that I can see what it looks like in real world usage. Otherwise, the only code I've seen that does something similar uses formal methods. So I simply do not believe that this is practical advice for most programming.

Insisting on examples and evidence to support an argument isn't combative. It's appropriate when extraordinary claims are being made.

If you've published code using this philosophy that is used by real people in real systems, then I would be happy to take a look at that as well. If it exists, I would bet it's in a niche of a niche.

I've had these arguments before about this very topic. Some people have taken me up on this request and actually provided examples. And in 100% of those cases, it turned out there was a mismatch between what they were saying and what the code was doing.

> I work for a FAANG but I’m not going to say which one. You or a relative are, with almost 100% certainty, relying on code written to that philosophy, by me, daily and widely.

Cool story bro.

Like, even interpreted maximally charitably, your statement still doesn’t provide GP’s requested published code. Not “take my word for it” ostensibly deployed software—code; the discussion here is about code constructs for modeling invariants, not solely about runtime behavior.

I’d be interested to see that code discussed in context of the blog post GP linked, which seems to make a compelling argument.

I am enjoined from providing that, and it’d be idiotic to risk my career for an HN ****-measuring contest. If one can’t understand these concepts without example code then this probably isn’t a discussion one can meaningfully contribute to.

Not being able to envision how it is in fact possible to write code with these invariants encoded in the type system is a fundamental fault in one’s ability to reason about this topic, and software correctness in general, in the first place.

> Not being able to envision how it is in fact possible to write code with these invariants encoded in the type system is a fundamental fault in one’s ability to reason about this topic, and software correctness in general, in the first place.

Code proving that it’s possible to avoid branching into an abort (the concept, not necessarily the syscall) was not what the original GP requested. Nor was a copy of your employer’s IP. Published examples which demonstrate how real-world code which intentionally calls panic() could be better written otherwise was my interpretation of the request.

And I’m requesting that, too, because I am interested in learning more about it! Please don’t assume I’m asking out of inexperience with safety critical systems, dick-measuring, faulty reasoning ability, or unfamiliarity with using type systems to avoid runtime errors (where—and this is the source of this discussion—practical and appropriate). If you work on your tone, that would make it much easier to have educating discussions in contexts like this.