81–90 of 93 posts
Earlier quoted context omitted.
Can't wait for dependently typed type systems
I've written code with dependently typed languages. It's very powerful, but it really is time-consuming. That won't be appropriate for all developments/developers.
That looks incredibly useful. Proving the absence of panics and overflows is already great, and with the annotations you can guarantee properties you'd normally write property tests for, like in this example from the docs: impl List { #[ensures(self.len() == old(self.len()) + 1)] pub fn push(&mut self, elem: i32) { // TODO } }
Can't wait for dependently typed type systems
Earlier quoted context omitted.
Nitpick, unsafe doesn't turn off the borrow checker. It just allows you to dereference raw pointers which are the things you must be careful about by reasoning about the actual safety yourself as a programmer. Everything else that uses safe pointers (references and mutable references) remain safe.
But how passing around a (constant) raw pointer is not sidestepping borrow checker? Since the pointer (AFAICT) does need to be borrowed, because it's manifestly immutable, it could be passed into several functions that alter the pointed-at memory in arbitrary order.
Earlier quoted context omitted.
Thanks for your interesting work! I wanted to ask, how are FFI boundaries handled? Are they ignored or is it an error to call FFI functions?
Currently they are not handled. But (you guessed it) we also have a project working on this: attaching trusted specifications to external methods. In the long term we might investigate a full integration with external verifiers, e.g. to check that the specifications declared on external methods in Rust is justified by their actual implementation, say in C. This is tricky because the specification language/level of ab…
Looks like I need to fix my binary search code!
- act as a C/C++ compiler for legacy code,
- shine where Rust is weakest: strings-first apps and apps that benefit from classes,
- get us to a world where the best C++ is a frozen C++
Too tall an order?
Looks like I need to fix my binary search code!
[off-topic] While you're at it, how about integrating D with cargo? D could: - act as a C/C++ compiler for legacy code, - shine where Rust is weakest: strings-first apps and apps that benefit from classes, - get us to a world where the best C++ is a frozen C++ Too tall an order?
Looks like I need to fix my binary search code!
[off-topic] While you're at it, how about integrating D with cargo? D could: - act as a C/C++ compiler for legacy code, - shine where Rust is weakest: strings-first apps and apps that benefit from classes, - get us to a world where the best C++ is a frozen C++ Too tall an order?
And what do you mean by Rust being weakest in these categories anyway, and why do you think it is? What are "string-first apps"? And how is not adopting inheritance-based OOP a weakness? I think, many experienced programmers, especially those familiar with ML family of languages and otherwise well-versed in different paradigms, will argue that this particular flavour of OOP is more harmful than helpful.
Why would you need a static analyzer for a language that promotes itself as safe out of the box.
This is a fair question really. Calling it a static analyser is misleading and seems to be editorialised. It's not like static analysers in C++. It's actually a formal verification tool. They call it a "static verifier" not a "static analyser". Most static analysis tools seek to find potential problems in your code - generally common mistakes - but they aren't proving anything usually. They have false positives and n…
- Prusti does not require you to write any "properties". I just ran it on a piece of code, which has no annotations for Prusti, and it still found a potential integer overflow. Maybe it has some internal annotations for std, but none for my code.
Earlier quoted context omitted.
[off-topic] While you're at it, how about integrating D with cargo? D could: - act as a C/C++ compiler for legacy code, - shine where Rust is weakest: strings-first apps and apps that benefit from classes, - get us to a world where the best C++ is a frozen C++ Too tall an order?
Sadly, D has its own set of problems and design flaws. It's better than C++ in many ways, but still far from Rust in terms of solid foundation in computer science and language design. Frankly, I see no point in integrating it with Rust. And what do you mean by Rust being weakest in these categories anyway, and why do you think it is? What are "string-first apps"? And how is not adopting inheritance-based OOP a weakne…
In other words, the human factors facet of language design. D does very well as a friendly language from a human factors perspective.
A simple example of this is `+` is commonly used to mean both addition and concatenation, leading to confusion with awkward resolutions. D uses `+` for addition, and `~` for concatenation. It's been working great.
We also regularly correct errors in the design of D.
Earlier quoted context omitted.
I've written code with dependently typed languages. It's very powerful, but it really is time-consuming. That won't be appropriate for all developments/developers.
Do you recommend any of the dependently typed languages more over others?