4 ms·

Nothing in Rust is an "experimental construct", so I'm not sure why you keep using that phrase. Lightweight formal tools like those available in Rust do guaran

• jstimpfle 9y ago
  > Nothing in Rust is an "experimental construct", so I'm not sure why you keep using that phrase. I don't do Rust (but I did some Haskell), and apart from the fact that both are very small elitist communities, some idioms are definitely evolving or changing as people try to find out what actually works in practice. So, from this practical standpoint, yes, experimental. What's lightweight lies in the eyes of the beholder. I certainly don't think of the line noise that is Rust code in the wild (again, to an outsider) as "lightweight". Nor do I think of the bazillions of ways you can obfuscate the simplest things in Haskell (moving 10, 20, or 90 percent of the perceived required invariants from value to type level), requiring large and possibly incompatible sets of language extensions, as lightweight. It's a burden of choice, and changing choices has huge ramifications on the rest of the code (these decisions are inherently unmodular, which is BAD). > No, languages that let you "iterate" and don't provide any sort of formal guarantees don't help you make correct code. They help you pump out a lot of mediocre code that probably works acceptably enough to satisfy a business with a medium-low focus on correctness. I'm sorry, but that's a very one-sided view. You can absolutely write correct code in them, and something that helps you to do it faster does help you write correct code. Simple as that. You seem to think that there is exactly one reasonable, justified level of formal correctness. And that is the level where you stand, Rust in this case. But that's wrong. Everything has a cost. And formalisms like Rust are still pityful attempts at constructing "formally correct" software. There might be some software that is "completely" verified, but at a cost that is simply not justifiable for the vast number of applications. Ignoring the fact that most real-world problems are ill-specified from the start. There is more than one valid approach to do things, and more so, to do many different things. It's cool what you're doing, but there are other valid approaches to find things to do and make them work. Get out of your little corner mate.
  • wyager 9y ago
    > both are very small elitist communities Yet another irrelevant, unjustified, negatively connoted description that has no basis in realty; first "experimental", now "elitist". Come on. > What's lightweight lies in the eyes of the beholder. In terms of formal methods that exist, both type systems simple enough for decidable inference and lifetimes are absolutely "lightweight". But sure, I guess every description is subjective. > You seem to think that there is exactly one reasonable, justified level of formal correctness. And that is the level where you stand, Rust in this case. This is untrue. I don't believe Rust is a paragon of correctness-oriented programming; I just think it's a hell of a lot better than something like Go. Rust at least lets you prove a sizeable chunk of practical safety and correctness properties. > And formalisms like Rust are still pityful attempts at constructing "formally correct" software. What Rust provides, including type and memory safety and completeness checking, gets you a surprisingly large way towards complete formal verification, imo. > Get out of your little corner mate. What was your goal with this statement? This is a fairly technical discussion, not a Reddit politics thread. There's no need for you to stoop to vague insults.
    • jstimpfle 9y ago
      > Rust at least lets you prove a sizeable chunk of practical safety and correctness properties. Not true in my perception. The things I do with conventional languages, I seldom worry about invariants that could be guaranteed by a more structural language, like null pointer safety or absence of side effects (I seldom worry about them because I seldom get them wrong). Much more I constantly juggle invariants like "this integer is a power of two and that integer is an odd positive one. This other pointer resource is the one that correlates with the integers in that specific way." These types of invariants are not practical to encode even in advanced type systems; I've even had a quick look and Agda and what-was-that-other-system-called, but it went quickly over my head. > Yet another irrelevant, unjustified, negatively connoted description that has no basis in realty; first "experimental", now "elitist". Come on. Not meant as an insult at all. >> Get out of your little corner mate. > What was your goal with this statement? This is a fairly technical discussion, not a Reddit politics thread. There's no need for you to stoop to vague insults. Dito. Your counter-arguments seemed to be heavily implying that there is no way way of getting code done correctly in a language that is somehow "lesser" than Rust. And furthermore you seemed to be preconceived about what others' judgement of the relevance of "correctness" is (which is a vague term - it sometimes seems to be more than "it runs correctly all the time and we could even prove it correct or actually have done so, even if not in some fancy modern type system"). So that little punchline at the end was not meant in an insulting way at all. Just to give note how your comments were perceived. Not that I really need to tell you, but it's good to admit other viewpoints / take interest how problems are typically approached in other domains. (By the way, I took an interest in John Carmack's recent engagements with static analysis and functional programming. I, for one, LOVE Carmack not only for being undoubtedly a genius who gets shit done, but furthermore for being so undogmatic about his approaches and views. You might have followed some of it, too -- for example, https://www.gamasutra.com/view/news/169296/Indepth_Functional_programming_in_C.php https://www.gamasutra.com/view/news/169296/Indepth_Functiona... , and it's also interesting to see that in the end he backed away after having seriously considered Haskell for game programming. I'm not sure if he backed away from his (actually existing) VRScript implementation written in (untyped) Racket as well)