HN Theater @HNTheaterMonth

Anyone is allowed to prefer a programming style that suits their aesthetics and habits, and like that one over all others. Aesthetic preferences are a very valid way to choose your programming language — ultimately that's how we all pick our favourite languages — and there's no need to make up universal empirical claims to support our preferences.

Here's a good talk to watch on the subject: https://youtu.be/ePCpq0AMyVk

And here's a summary of various studies done: https://danluu.com/empirical-pl/

As of today, what we know is that if there's a positive effect of types on correctness, then it is probably a small one.

There's really no need to assert what is really a conjecture, let alone one that's been examined and has not been verified. If you believe the conjecture is intrinsically hard to verify, you're conceding that you're only claiming a small effect at best (big effects are typically not hard to verify), and so there's even less justification for continuing to assert it. It's okay to prefer typed languages even though they do not, as far as we know, have a big impact on correctness.

⬐ Tainnor

I'm not sure if that's true, even big effects can be hard to verify if there are significant confounders.

For example, let's imagine that writing OCaml code really leads to fewer bugs than writing code in Lisp (to just choose two languages) but only after you've trained people in OCaml for ten years. Or maybe, technically Java leads to measurably fewer bugs than Ruby, but because most popular Java projects make heavy use of reflection, the effect dissipates... and so on (these are just examples for potential confounders, I'm not claiming they're true).

You are correct that one cannot claim that "static typing leads to fewer bugs" is a demonstrably correct statement, but I don't think you can claim that there demonstrably can be no (big) effect either. And in the end, you're also allowed to believe in conjectures even when there is no solid evidence behind it. People do that all the time, even scientists.

⬐ pron

You can believe in such a conjectures, but it's wise to consider the more probable possiblity that if an effect hasn't been found, then it is likely small.

Also, in the end it doesn't really matter, because the conjecture that's repeated as an assertion isn't said merely as a scientific claim, but as an attempt to convince. Companies are interested in some bottom line effect, and rather than trying to sell your favourite approach with something like, "I like it; maybe you'll like it, too", you make some unsupported assertion that goes like this: "you should use my thing because it will actually make an important contribution to some bottom-line effect you're interested in; oh, and by the way, you might not notice it." That isn't convincing at all, so it's best to stick with what we know: "I like it, maybe you'll like it, too."

⬐ Tainnor

Show me the companies that only ever implement policies that have shown to be effective in rigorous empirical studies.

Usually some person (or a group of people) is in charge of some decision and that person will make judgment calls based on their beliefs. This is no less true of programming techniques than it is of management styles, corporate strategy or anything else.

Your insistence that we may not have beliefs about the very things we work with daily, unless they're empirically verified, is IMHO frankly ridiculous.

⬐ pron

That's not my insistence at all. You can believe what you like. What you can't do is make empirical assertions that we've not been able to validate empirically.

Companies may adopt a technique based on empirical findings or anything else they like; most people choose a favourite programming language because they like working with it better. But the statement that types lead to fewer bugs is a very particular assertion that is simply unsupported by evidence. You may believe that using types reduces baldness and make your choices based on that, but it's still a conjecture/belief at best.

⬐ Tainnor

I think you're guilty yourself of what you're accusing other people of.

I haven't seen people ITT arguing that there is empirical evidence for types providing better correctness guarantees, just that they strongly believe it to be the case given their own experience.

⬐ pron

The original statement was "A language with static types would have made it easier to build correct software." This is an empirical claim that the evidence does not support. Note that it's not that there's merely no evidence supporting the claim, but that studies designed to support the claim failed to do so.

⬐ ThenAsNow

  Anyone is allowed to prefer a programming style that suits their aesthetics and habits, and like that one over all others. Aesthetic preferences are a very valid way to choose your programming language — ultimately that's how we all pick our favourite languages — and there's no need to make up universal empirical claims to support our preferences.

That's fine, but I'm not sure what it has to do with my comment as it was not about preferences based on aesthetics or habits.

Thanks for the links though.

  There's really no need to assert what is really a conjecture, let alone one that's been examined and has not been verified.

There's no unsupported conjecture in "it is strictly more rigorous to catch equivalent bugs through the interpreter/compiler than through testing or other runtime-dependent approaches."

  If you believe the conjecture is intrinsically hard to verify, you're conceding that you're only claiming a small effect at best (big effects are typically not hard to verify), and so there's even less justification for continuing to assert it.

It's easy to fall victim to the Robert McNamara fallacy, that if something isn't easy to measure its effect or importance is insignificant. Anyone looking back at U.S. defense and procurement policy from his era is free to observe the lack of real-world congruence with such thinking. The Dan Luu page you cited, more than anything else, seems to reinforce that the cited studies are hard to interpret for any rigorous conclusions or for validity of methodology.

This is why I did not make sweeping statements along the lines of "the majority of dynamically-typed software in production [no qualifier on what "production" means] would have fewer bugs if it were statically-typed" or the like.

⬐ pron

> That's fine, but I'm not sure what it has to do with my comment as it was not about preferences based on aesthetics or habits.

Because you made the claim that "it is strictly more rigorous to catch equivalent bugs through the interpreter/compiler than through testing or other runtime-dependent approaches," but that claim was simply not found to be true.

> There's no unsupported conjecture in "it is strictly more rigorous to catch equivalent bugs through the interpreter/compiler than through testing or other runtime-dependent approaches."

There is, unless you define "more rigorous" in a tautological way. It does not seem to be the case that soundly enforcing constraints at compile time always leads to fewer bugs.

> It's easy to fall victim to the Robert McNamara fallacy, that if something isn't easy to measure its effect or importance is insignificant.

The statement, "you will have fewer bugs but won't be able to notice it," is unconvincing. For one, if you can't measure it, you can't keep asserting it. At best you can say you believe that to be the case. For another, we care about the effects we can see. If the effect doesn't have a noticeable impact, it doesn't really matter if it exists or not (and we haven't even been able to show that a large effect exists).

That the effect is small is still the likeliest explanation, but even if you have others, your conjecture is still conjecture until it is actually verified.

> The Dan Luu page you cited, more than anything else, seems to reinforce that the cited studies are hard to interpret for any rigorous conclusions or for validity of methodology.

It does support my main point that despite our attempts, we have not been able to show that types actually lead to significantly fewer bugs, i.e. that the approach is "more rigorous" in some useful sense.

> but it is certainly not as straightforward as you make it seem.

I never claimed it is straightforward; it is anything but. As a practitioner and advocate of formal methods and verification, I've been following research in software correctness for many years (and have written much about it, e.g. https://pron.github.io/posts/correctness-and-complexity), I've come to realise how complex the problem is, and there's more we don't know than we know, and even the things we know are problems, we don't know what the best solution is, because often solutions carry with them more problems.

Nonetheless, there are certain principles. We know that we can eliminate certain bugs with compile time guarantees; we also know that code reviews catch many (many!) bugs, and so making them easier helps. But what if these two are in opposition? It's not easy to tell which wins in which circumstances.

> In the end though, for the Zig case I agree that the jury is still out.

True, but the jury is still out on Rust, too. In fact, for most languages. However, there is no clear argument that we should assume, a priori, that Rust results in more correct programs than Zig. Many such arguments in the past have failed to yield positive empirical results (e.g. https://youtu.be/ePCpq0AMyVk). In fact, given empirical research, the safest bet is to assume the null hypothesis -- that there is no difference. Out of an abundance of caution, I'll assume that languages whose designers place a strong emphasis on correctness might achieve it more easily than languages whose designers put no emphasis on it at all, but Zig and Rust are in the same category here. Both are designed with correctness as a primary goal. But as their design and means of achieving correctness is so different, I think it's impossible to make an educated guess as to which of them, if any, yields more correctness more easily.

If we want some bottom line, it is this: software correctness is so complex, and solutions are often so non-obvious (i.e. many work in theory but not in practice), that we cannot say anything with certainty until we have actual empirical results, and even then we need to be careful not to be careful not to extrapolate from one study to other circumstances with different conditions (i.e. that TypeScript seems to have fewer bugs than JavaScript does not seem to extrapolate to the general claim that typing always reduces bugs compared to no typing in the same amount or at all, when other languages are concerned).

⬐ littlestymaar

> We know that we can eliminate certain bugs with compile time guarantees; we also know that code reviews catch many (many!) bugs, and so making them easier helps. But what if these two are in opposition? It's not easy to tell which wins in which circumstances.

I understand the argument, but I'm not sure on what basis you consider that Rust's type system harms code review. Do you have specific examples in mind? (And because the discussion is about Zig, this is a pretty strange argument to make, because Zig's ubiquitous usage of metaprogramming is in fact a hindrance to code review).

⬐ pron

Rust is easily among the top five most complex programming languages ever created (it's in the good company of other low-level languages that follow a similar design philosophy, like C++ and Ada).

Calling Zig's comptime "metaprogramming" is a little misleading when compared to other low-level languages. It is used for the same purpose as metaprogramming in other low-level languages (like macros in C++ and Rust, or templates in C++), but doesn't have any quoting mechanism [1] and doesn't operate at any "higher-level." In fact, Zig's semantics would be unchanged if comptime were executed at runtime. It is more similar to meaprogramming in dynamic language with reflection, with the benefit that related "runtime" errors are actually reported at compile-time. So comptime doesn't increase Zig's complexity. It can be thought of as a pure optimisation.

[1]: Unlike metaprogramming in Rust or C++, Zig's comptime is referentially transparent, i.e. if two terms, x and y, have the same meaning, then, unlike in C++ or Rust, one cannot write a unit e in Zig, such that e(x) and e(y) have different meanings. So the metaprogramming features in C++/Rust are trickier than Zig's.

⬐ littlestymaar

> Rust is easily among the top five most complex programming languages ever created

You said that already[1], this is unsubstantiated and you declined to answer to my rebuttal.

> So comptime doesn't increase Zig's complexity. It can be thought of as a pure optimisation.

I'll grant you that it doesn't increase Zig's implementation complexity and also have a smaller learning-curve cost than other mecanisms. But when reading a piece of Zig code, you constantly have to wonder at which time the given code is gonna run. And there's much, much, more comptime in use in any piece of Zig code, than you'll uncounter macros in Rust or C++. So yes, it adds its share of friction when reading Zig code.

[1]: https://news.ycombinator.com/item?id=26511584

⬐ defen

> You said that already[1], this is unsubstantiated and you declined to answer to my rebuttal.

How would you propose to measure the concept of "programming language complexity"? One metric could be "how difficult is it to write programs that do not contain certain classes of bugs"? By that metric, C is indeed incredibly complex. An alternate metric might be "how long does it take the average developer to learn the language well enough to write reasonably effective programs"?

In the absence of formal studies we just have to go by our intuition. Personally, I kinda hate the "I'm not smart enough to write C, so I write Haskell/Rust" argument. It comes across as incredibly condescending to me. What I can tell you from my experience is that I spent a month trying to learn Rust on nights and weekends, and by the end of that was able to write some extremely simple programs with a lot of effort. On the other hand I was making nontrivial contributions to Zig itself within a week of learning the language. So to me, Rust is much more complex than Zig.

⬐ littlestymaar

I'm not a native English speaker, but as far as I know, the word complexity in English is pretty close to its meaning in French (where it comes from). From Wikipedia:

> Complexity characterises the behaviour of a system or model whose components interact in multiple ways and follow local rules, meaning there is no reasonable higher instruction to define the various possible interactions.

This is in fact the most antithetical possible description of Rust, which, thanks to its strong type system and compile-time rules, keep the interactions between different components or features as clear and specified as possible.

Yes Rust is hard to learn, but learning curve and complexity are orthogonal concerns.

⬐ pron

> You said that already[1], this is unsubstantiated and you declined to answer to my rebuttal.

Sorry, didn't see your response. I can answer it in two ways, subjective and objective. The subjective is "I know it when I see it," which roughly corresponds to the difficulty in determining what an unfamiliar piece of code does as well as how many language rules I need to know to figure that out. The objective one is literally language complexity, i.e. the computational complexity of determining whether a string belongs is in the language or not (i.e. whether or not it is well-formed).[1]

> you constantly have to wonder at which time the given code is gonna run

You really don't. The semantics of Zig are the same as those of Zig', which would be the language that runs comptime at runtime. The whole point of comptime is that as far as semantics -- not performance -- is concerned, you do not have to care when code would run.

[1]: There's a complex theoretical caveat here, because I believe both Zig and Rust are undecidable. So we can exclude degenerate cases from Rust, and look at the complexity of Zig' , the language I introduce in the second paragraph, which is semantically the same as Zig.

⬐ littlestymaar

That's a strange vision of the burden of proof.

Anyway, complexity can come from many factors:

- feature bloat: C++ is way more complex now than it was in 1990, because features where added on top of features. In that regard, the older a language gets, the more complex it becomes. C++ is the most cited example, but I think PHP is even worse in that regard: it's probably the one and only most feature bloated PL ever, probably because there is not even a standardization committee to add frictions to the feature additions process. By that metric, Rust is slowly becoming more complex every year, like every other language (but the growth of its complexity isn't particularly concerning compared to others, Go for instance has recently been on a much steeper track).

- platform fragmentation: when Internet Explorer was still a thing, JavaScript development was made incredibly complex by the huge implementations differences between browsers. Code that worked somewhere failed somewhere else more often than not, and you had to keep work-around for old versions or IE for years. IE is mostly dead, Safari is less shitty every year, and google killed Android Browser and replaced it with Chrome, so it's a much smaller issue than before, but problems remain.

- cultural factors: Haskellers love for obscure mathematical terms or the fetishism of OOP's design patterns in Java in the late-90 and 2000 are good examples of culturally-induced complexity.

- ecosystem churn: JavaScript between 2013 and 2018 or something, with new framework or libraries or tools replacing the old ones every six months, before getting replaced themselves in the following month was a massive source of complexity, fortunately it seems to have settled a bit and the churn rate is lower than before. In Rust's early days, when many useful features were still unstable and feature-gated in the nightly version of the compiler, this phenomenon also existed (though at a much smaller scale). By that metric, Rust's complexity decreased quite a bit since 1.0, as many libraries have been adopted as de facto standard way of solving a bunch of problems (a few domains remain prone to this though, like error handling helpers, and ECS for game engines apparently) and Rust is now roughly in the same situation as most languages.

- counter-intuitive semantics: c.f. pre-ES6 JavaScript, how `this` and `var` bindings worked, which was simply the opposite of what people wanted in 95% of the cases.

- obscure control flow: `with` statement in non “strict mode” JavaScript, languages relying on a lot of `goto`, or even languages with exceptions.

- too much responsibility: manual memory management in C (or Zig for that matter) which we now have significant evidence after half a century that no human is able to do it consistently right of the time.

- poor interactions between features: see C++, how modern features interact poorly with older (more C-like) ones.

Rust is less complex than many mainstream languages on a least one of these dimensions, and less complex than JavaScript on most of these…

> The objective one is literally language complexity, i.e. the computational complexity of determining whether a string belongs is in the language or not (i.e. whether or not it is well-formed).[1]

This is a stupid metric, because it confuses implementation complexity with user-facing complexity (brainfuck wins this benchmark, yet good luck building anything with it). But from a theoretical perspective, this is a fun one because there's not only one but two classes of indecidability involved:

First, with most language with type polymorphism, it is undecidable to know whether a given program will successfully compile. But there's also a second level: when a language has Undefined Behaviors, a program compiling successfully isn't enough: it can still be invalid, and whether or not it is valid is also undecidable. C is not in the former situation but is in the later, C++ and Zig are in both, safe Rust is in the first only, but unsafe Rust is also in both. So in that regard, safe Rust is strictly less complex than Zig, but the whole Rust is equivalent.

> You really don't. The semantics of Zig are the same as those of Zig', which would be the language that runs comptime at runtime. The whole point of comptime is that as far as semantics -- not performance -- is concerned, you do not have to care when code would run.

This argument is pretty similar to the Rust point of “when you get used to it, ownership doesn't adds any cognitive burden”, maybe when gaining enough familiarity with Zig you can gloss over it without hassle, but I'm clearly not in this case yet so you really better not assume that it's gonna be straightforward and instantaneous for everybody, it is not.

⬐ pron

> That's a strange vision of the burden of proof.

I don't think so, because I don't think I'm claiming what you think I am.

> Anyway, complexity can come from many factors:

I completely agree, but I'm only talking about language complexity, in the strict syntactic, linguistic sense. I am not saying that all things considered, Rust makes maintaining programs harder than other languages -- nobody knows that until we have some empirical study -- but linguistic complexity is one very prominent property of Rust, as is, say, the memory safety of safe Rust, which, similarly, does not mean that Rust programs are overall safer than those written in, say, Zig, when all things are considered, because correctness also has many contributors, not just sound syntactic guarantees. There, too, only empirical study can settle the issue.

But you can't have it both ways, focusing on one specific piece when it comes to correctness yet insist on looking at the full picture only when it comes to complexity. All you can say is that, linguistically/syntactically, Rust offers some sound guarantees re memory safety and that it is complex, and that overall, both subjects are complex, involve many aspects, and require empirical study to make any definitive claim about.

> This is a stupid metric, because it confuses implementation complexity with user-facing complexity

It is obviously not stupid because it is commonly and usefully employed in computer science. But as with any precise definitions, it focuses on some aspects and not others. It captures the intrinsic difficulty of answering a question about a program. You are correct that it does not take into account human ergonomics and psychological aspects, but it is one more useful metric, even if not comprehensive.

> This argument is pretty similar to the Rust point of “when you get used to it, ownership doesn't adds any cognitive burden”,

Absolutely not (and, BTW, I was not referring just to ownership and lifetime when I spoke of Rust's complexity). It is a very precise and well defined property of Zig. The semantics of a Zig program, i.e. what it does in terms of what action it computes, is completely independent of comptime. It is not an ergonomic or psychological argument. comptime does not change the meaning of anything, and not only do you not need to figure out what happens at compile time and what happens at runtime -- unless you want to reason about efficiency -- but that knowledge contributes nothing. It's a meaningless distinction when it comes to semantics. It's a very powerful, well thought-out, theoretical and practical aspect of Zig's design.

⬐ littlestymaar

> but I'm only talking about language complexity, in the strict syntactic, linguistic sense.

Then again, on the strict syntactic sense, Rust is even less complex than C, because of the “most vexing parse” issue. If you wanted a rigorous analysis of the syntactic complexity, you could attempt to measure how difficult it is to write a lexer and a parser for every popular languages, and see how Rust performs. But given that the language grammar has been designed with parsing complexity in mind and have benefited from the hindsight of others before it, you'd be terribly disappointed.

From this discussion, and many of your previous interventions on this forum, it's pretty clear, even though the reason isn't, that you have developed a resentment towards Rust and you can't help bashing it.

Rust isn't a silver bullet, it has a fairly tough learning curve and as it tries to push the frontier of system programming language forward, it will take a few decisions that will ultimately be regarded as dead ends, and I have no doubt that future languages will avoids these pitfalls and provide improvement over the state of the art.

In the meantime, spreading your hate with unsubstantiated judgements like “Rust is one of the 5 most complex programming language ever” or “Rust harm code reviews” isn't really constructive for anyone.

Zig is a cool motorbike, Rust is a SUV. Arguing that your bike can indeed be safer than a SUV because you have more visibility and agility to avoid the danger is beyond childish.

Super easy cross compilation and incredible development velocity on small-medium projects are super cool features of Zig, and Rust can't beat that. No need to downplay the importance of Rust for the software industry (and as a friendly reminder, Rust is making its way to the Linux kernel, with the approval of Linus because unlike C++ or Ada isn't too complex to his taste ;).

⬐ pron

> can't help bashing it.

Perhaps this may disappoint you, but I -- like many and perhaps most developers -- don't get such emotional responses, positive or negative to any programming language [1], which might appear as resentment to the emotionally attached. I am very impressed with some aspects of Rust, less impressed with others, and overall, my feelings toward it overall are shaped just like yours: by personal aesthetics. I don't find Rust's aesthetics very appealing and so Rust isn't my cup of tea (although I would't resent working in it because I'm not emotional toward languages and I currently program mostly in a language whose aesthetics I like even less than Rust's [2]), while you find them appealing and so you do like Rust. It's all just a matter of taste, and I fully accept that not everyone shares mine. I think your approach is too coloured by emotion, and is therefore unconstructive. You're a zealot, and you project that attitude on others, so "unconvinced" appears to you as a personal attack, and scepticism or dislike seems to you like bashing.

> Rust is even less complex than C, because of the “most vexing parse” issue. If you wanted a rigorous analysis of the syntactic complexity, you could attempt to measure how difficult it is to write a lexer and a parser for every popular languages, and see how Rust performs

No. The complexity of a formal language, like that of any set, is the computational complexity of deciding whether a string is in the language (so, including type-checking), not as the complexity of the parsing phase (https://en.wikipedia.org/wiki/Computational_complexity_theor...). I'm not saying this is the most useful way to talk about language complexity in this context (and caveats are needed, anyway, to make a more fine distinction between languages), but that is certainly one well-known way to talk about the intrinsic complexity of a language.

> Zig is a cool motorbike, Rust is a SUV. Arguing that your bike can indeed be safer than a SUV because you have more visibility and agility to avoid the danger is beyond childish.

It is beyond childish to make such inane statements about software correctness when you're clearly not very familiar with the subject, and are drawn to arguments like "more correctness => more soundness". The effect of language design on correctness is a complex subject with mostly unsatisfying answers, and even in software verification research, the debate over the value of soundness is far from settled (and not currently leaning toward more soundness). An equally inane statement would be, "Zig is like a modern aeroplane, relying on multiple levels of safety, some mechanical and some human, while Rust is like an old train that breaks down and kills everyone once there's a problem with the tracks." If we've learned anything about software correctness in the past decade it's that there is not much we can assume in advance, and that we don't really know one best way to improve it. It is true that some researchers think that the best answer to any correctness issue is more soundness in the language, but not only is this not a consensus opinion, I doubt it's even a majority opinion.

[1]: I would say I'm a "language sceptic." I'm generally sceptical toward any empirical claim about the bottom-line effectiveness of linguistic features without empirical support, and overall think that whatever empirical studies we do have show little impact overall to language design (comparing "reasonable" alternatives, at least), certainly compared to what all language fans claim. I would never, say, make a definitive claim like, "Zig yields more correct programs than Rust", or "Rust yields more correct programs than Zig," without clear empirical support (and my guess based on prior results would be that they're about the same).

[2]: C++

⬐ littlestymaar

> I think your approach is too coloured by emotion, and is therefore unconstructive.

Your little “I'm a rational agent, you are too emotional” is pretty cute. But it would work better if your whole attitude in this thread didn't contradicted it, don't you think? “Rust is among the five most complex language” is not a rational argument, it's a personal feeling. Why you feel the need to spread your feelings over the internet while pretending you're not an “emotional” person is quite intriguing. If you want to look more like a rational person (no human really is), try to keep as much personal and unsubstantiated judgement out of your writings.

“Rust marketing makes safety claims that we should not take at face values” is alright, “Rust is one of the five most complex language ever” doesn't pass this test.

> is the computational complexity of deciding whether a string is in the language (so, including type-checking)

But for both Rust, C, Zig, and many others, it's undecidable, so by this definition of complexity, these language are definitely too complex (and equally so).[1] In fact, your desperate attempt to save your initial argument about complexity, by narrowing it to a tiny technical corner makes me cringe a bit.

> I would never, say, make a definitive claim like, "Zig yields more correct programs than Rust", or "Rust yields more correct programs than Zig," without clear empirical support (and my guess based on prior results would be that they're about the same).

The technicality of what constitute a “definitive claim” in a human to human conversation is an interesting question, but in practice truisms like “we can't conclude whether Rust is safer than C” or “we can't conclude that Rust doesn't bring more bugs than Zig does” aren't neutral: what such claim attempts to do is insinuate the opposite. And when combined with gratuitous judgements like “Rust is one of the 5 most complex language ever”, it looks a lot like an attempt to deter people from using this language you don't like. (And now I have a clue on what the root cause of your bad feelings can be).

[1] And as I said earlier, in the case of Zig and unsafe Rust and it's not just about type-checking: because of UB, even after compilation whether the compiled binary is the binary of a valid program or not is also undecidable.

⬐ pron

> But for both Rust, C, Zig, and many others, it's undecidable, so by this definition of complexity, these language are definitely too complex (and equally so)

My comments on this tried to be as careful and as precise as possible, and touched on this very issue.

> In fact, your desperate attempt to save your initial argument about complexity, by narrowing it to a tiny technical corner makes me cringe a bit.

Your emotional response here is so powerful that I think we're conversing on entirely different levels. I am sorry if my mild and careful statements have touched on something that you clearly see as essential to your identity.

> aren't neutral: what such claim attempts to do is insinuate the opposite

No. It is the most precise and careful statement that I can say, having followed the research for years and being a practitioner and advocate of formal formal methods. Anything I say, the more careful I try to be, it just seems to send you into further rage (and abuse). I think you're in a middle of a tantrum that's clouded your judgment, or perhaps, being a zealot, you cannot imagine any other attitude. Anyway, this conversation is making me very uncomfortable, as I sense you're in a very agitated emotional state, and I want no part of that.

⬐ littlestymaar

> No. I think you're in a middle of a tantrum and that's clouded your judgment.

I have to admit, this is cool rage-quit punchline!

Edit:

> I am sorry if my mild and careful statements have touched on something that you clearly see as essential to your identity, but I simply see no way to discuss this subject with you.

> Anyway, this conversation is making me very uncomfortable, as I sense you're in a very agitated emotional state, and I want no part of that.

Wow, it got even better as I refreshed the page!

⬐ HourglassFR

> (and have written much about it, e.g. https://pron.github.io/posts/correctness-and-complexity)

Wow, thanks for that link. I only made it through the first part for the moment but it is an incredible read. You clearly thought about this more deeply and carefully than I did.

Edit: I'm not entirely sure how that came across so I want to explicitly say that this is not a dry ironic statement (communication is hard, and I am a poor writer).

⬐ pron

If there's anything I learned it is to be wary of any easy answers or definitive claims when it comes to software correctness.

⬐ dnautics

Are you interested in helping kickstart interest into formal verification of zig? My contact info in profile.