5 ms·
Needs a companion blog, "perfectly safe code the rust compiler will nag you about". And the contortions rust programmers go through to avoid that. Rust is real
by LAC-Tech 5y ago
Needs a companion blog, "perfectly safe code the rust compiler will nag you about". And the contortions rust programmers go through to avoid that.
Rust is really impressive in a lot of ways. Type classes and pattern are a great fit for systems programming.
But they're fixated on the idea that everything possible should be a static analysis error, language ergonomics or usability be damned. I'd much rather these be warnings, because no static analysis on earth is going to stop you from actually needing tests to see if your code works.
- rhn_mk1 5y ago> no static analysis on earth is going to stop you from actually needing tests to see if your code works. I might have been convinced if mathematical proofs were not expressed in code. If a proof can exhaustively cover the problem space, then there's no need for further testing. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- LAC-Tech 5y agoFair point, but would you deploy un-tested code to production based on a static proof? AFAIK the issue with this stuff is that the kinds of problems proofs are able to practically cover are very small. Static analysis is an incredibly useful tool, not denying it. I am saying we should avoid worshipping at its altar. Any useful program is incredibly complicated and needs some kind of run time testing.
- yazaddaruvala 5y agoI don't feel like static analysis and unit testing are very different things. Given that my unit tests run roughly at compile time (ideally they would run during compile), it really isn't different than static analysis. Especially unit tests where all the inputs are mocked and expected outputs are provided. When I wrote Ruby/Javascript, I remember needing to write unit tests that verified types of input/output variables. These kinda tests were undifferentiated boilerplate that needed to exist but didn't need to be written by me. Especially since there were many tests I'd forget to add or would intentionally not add because the test file was getting obnoxiously large. Factoring out those boilerplate tests into the compiler (when using Java, Rust, or TypeScript) was very valuable to me, but didn't change the fact that they are basically automatically generated unit tests. The borrow checker in Rust is a similar factoring out of automatically generated unit tests, which I wouldn't have typically written. Continuing to push more undifferentiated unit testing into the compiler/libs/proofs helps make sure I only need to write domain specific unit tests. Why do you feel static analysis and compile time unit testing are different? or do you mean, domain agnostic testing is ok, but really we need domain specific testing?
- LAC-Tech 5y agoWhen I wrote Ruby/Javascript, I remember needing to write unit tests that verified types of input/output variables. When I write in dynamically typed language I never write tests like that. I'm more familiar with static than dynamic, but are experts really doing that kind of thing? That'd be a case for design by contract.
- rhn_mk1 5y agoSure, sometimes I even deploy code without a proof nor tests ;) Jokes aside, if my problem is small enough to be proved (for whatever value of small), I do not see any more value to be extracted from tests. Who bothers checking that 3+2 = 2+3 after proving that x+y = y+x?
- emerged 5y agoI took computer language theory in college literally 20 years ago, had a sandwich with chips during every class. I clicked on that link and could taste the sandwich.
- AlotOfReading 5y agoI wish static analysis were always sufficient. Curry-howard doesn't obviate the need for tests. Anything affected by the physical implementation of the computer still needs to be tested, for example. That includes corruption safety for databases, timing side channels in cryptography, all high-integrity code, and so on. Proofs can also be buggy themselves, as can the verifiers. But yes, formal methods make testing a lot easier and taken far enough, can suffice on their own.
- rhn_mk1 5y ago> Anything affected by the physical implementation of the computer still needs to be tested, for example. That includes corruption safety for databases I think that comes under "taken far enough". If you can model the corruption in your proof, you're good. I'm less confident about timings. But you're right that testing is still useful for bugs on other levels. After all, going high enough, humans can have buggy requirements, and no proof will catch that. Tests might.
- jonpalmisc 5y agoDo you have any examples of the “perfectly safe code the Rust compiler will nag you about”? Not trying to start language wars, just genuinely curious as someone who writes Rust on occasion.
- tayo42 5y agoI dont have an example in front of me. I had write some weird code to prevent a variable from being dropped unexpectedly.
- ben0x539 5y agomy go-to example is the non-lexical lifetimes stuff, like when you're somewhere in a match and you don't get to return a reference to a thing because there's another reference that's clearly not relevant anymore at the top of the match
- kibwen 5y agoThough it's worth mentioning that Rust gained support for many non-lexical lifetime patterns a few years ago, and has designs on supporting more in the future.
- melissalobos 5y ago> Do you have any examples of the “perfectly safe code the Rust compiler will nag you about”? Not an example, but if the borrow checker approved every proper program in a reasonable time, then it could solve the halting problem.
- 5y ago
- verdagon 5y agoSomething I find interesting about Rust is that we can do those safe patterns, as long as we're willing to lose some performance. The way I think of it: Rust forces us to choose between flexibility and zero-cost memory safety. If we choose zero-cost memory safety (in other words, we don't use Rc or unsafe or large Cells) we can't do things like dependency injection, basic observers, backreferences, many kinds of custom RAII, etc. But we do get speed. On the other hand, if we allow e.g. Rc into our codebases, we can do these patterns just fine, though there is a performance hit. The final challenge in learning Rust (IMO) is to figure out when Rc is better, and when we can afford the complexity cost of zero-cost memory safety. I've seen a lot of Rust projects move mountains to avoid Rc, and ironically end up adding more run-time overhead and complexity.
- cranky908canuck 5y ago> On the other hand, if we allow e.g. Rc into our codebases, we can do these patterns just fine, though there is a performance hit. Interesting... I was using one of the Project Euler problems as an exercise for learning Rust; I found that Rc actually improved performance (guess: by eliminating a lot of copies/moves as things went in and out of scope).
- deleted 5y ago[deleted]
- eximius 5y agoMaybe you should have been using more immutable references? But I'm actually curious why the compiler would be making many copies after optimization passes. Release builds or debug builds?
- ridiculous_fish 5y agoIf you try to code Rust like JavaScript by using Rc everywhere, you will quickly run into panics when you try to borrow from a RefCell that a caller has also borrowed from. The limitations of &mut cannot be trivially worked around.
- cranky908canuck 5y ago> ... no static analysis on earth is going to stop you from actually needing tests to see if your code works. Correct. However, the intent of Rust is that the code will not fail [1] due to some silly machine thing below your current level of abstraction. As an example, I'd point to one thing that Rust does that solves a lot of problems: the Vector. This gives you: - a buffer to load as needed - bounded memory usage ( no more than 2x what's actually needed, and the ability to tailor it) - automatic resizing as needed IOW, eliminates 'C programmers disease' (eg: #define BUFFERSIZE 1024 // big enough for anything :-) ) I am sick and tired of writing either the tedious resizing stuff by hand, or using a linked list [2] (which in today's world isn't performant: a self-resizing array will deal with locality-of-reference issues much better). Disclaimer: I've only peripherally used Rust professionally (ie., corporate innovation sessions, self-contained utilities). I have done enough 'fitness exercise' stuff that I'm confident to comment. [1] "Fail" as in, do something random like start a cryptominer at root-level-privilege. "Fail to compile" is fine, "panic at runtime" is not fine but not worst case. [2] Opinion: the reason why linked-lists are an example of something hard to do in Rust is because Vectors make them irrelevant, so why bother?
- oynqr 5y agoWho forces you to keep rewriting a vector in C?
- ben-schaaf 5y agoThe lack of generics/templating in C.
- mvolfik 5y agoVectors really don't make linked lists irrelevant - if you want to be able to quickly pop from the middle, no Vec magic will currently help you
- adgjlsfhk1 5y agoVectors by themselves don't make linked lists irrelevant, but they remove 90% of the use cases, and most of the remaining ones would be better served by a hashtable, or some sort of fancy tree. Linked lists (especially as C programmers typically implement them) are absolutely awful for performance.
- oxff 5y agoIt is very ergonomic language though, when you consider how much of C++ complexity it manages to simplify. > I'd much rather these be warnings Delusional attitude. If it can be caught at compile time it should be; there is no reason to leave it as a warning for programmer to maybe handle.
- pjmlp 5y agoFor some schizophrenic reason, when I look at GAT proposals or macros, I rather be dealing with C++ code.
- DeathArrow 5y agoC++ can be as simple as you want.
- golergka 5y agoThere's unsafe for that.
- Dowwie 5y agoThere's a very good chance that in whatever language you're using you're not testing remotely close to what you'd need to in order to reach parity with that of the rust compiler. It's very Dunning-Kruger of a developer to believe that they are achieving such a level of edge case testing.