Comment by mrkeen
11 days ago
Type systems are hard! Check out https://counterexamples.org/
I gave it a quick scan for Rust examples; there are 11 samples among the following pages:
https://counterexamples.org/eventually-nothing.html
https://counterexamples.org/mutable-matching.html
https://counterexamples.org/selfishness.html
https://counterexamples.org/scope-escape.html
https://counterexamples.org/nearly-universal.html
The first thing I always look for is mutability (combined with some other tricky feature), e.g. "Now it's a Just(3):Maybe<Int>, now it's a Nothing:Maybe<Int>, now it's a Nothing:Maybe<String>."
I wonder if TFA's example could be reproduced without mutability.
https://github.com/JelleZijlstra/unsoundness is also a great collection of Python type system holes. In these cases, it's mostly deliberate design decisions, not bugs. The unfortunate fact is that a fully sound Python type system would be a pain to use.
> The unfortunate fact is that a fully sound Python type system would be a pain to use.
Even beyond Python, most gradual type systems are unsound by design.
Perhaps I'm just an old dog that doesn't want to learn new tricks, but I still can't think of Python as typed and I never use type hints. I started with Python during the 2.3 era. I still view Python types as merely docs. So it's nice that someone tracks mypy quirks but I can't imagine relying on the results for anything serious.
I've been writing python for closing in on two decades (I want to say maybe 2.5 was my introduction point?).
I've found type hints to be remarkably useful and catch significantly more bugs than I ever would have thought, and have quickly picked up the practice of using them wherever I code. My general finding is that if I have to struggle to put useful type hints in place, I probably need to rethink my code.
I even type hint my unit tests because I've learned that sometimes type incorrectness means my tests haven't been testing what I thought they were testing.
Frameworks like pydantic[0] can help you turn those type hints into something runtime enforcing too.
[0] https://pydantic.dev/docs/validation/latest/get-started/
1 reply →
If you deal mainly with small-to-medium size Python programs, which is probably the norm, that makes sense to me. But if you have a large Python application, or if you own a library API that might have a lot of callers, typecheckers catch sooo many mistakes.
1 reply →
You can't rely on Python's type hints for serious verification, but it can be great for expressing abstractions and giving people (and, today, agents) better affordances for using them. Even static errors that will not always fire can still help a lot for using a library correctly and for noticing mismatches in your codebase as it evolves over time.
To be very pedantic, Python was always strongly typed in the sense that every value has a concrete type. This is very different to, e.g. C, where `void*` is often used to actually erase the type or, conversely, more abstract languages where there are only interfaces.
But of course Python function were always duck typed so it often didn't matter to the user.
1 reply →
> Check out https://news.ycombinator.com/item?id=27252899 - May 2021 (62 comments)
Aren’t some type systems (eg Lean) able to essentially verify/prove arbitrary mathematics?
Yes, until you introduce inconsistent axioms. Then you can prove anything.
"Type systems are hard!" As hard as its safety is pushed on us, not even Rust is free from hand waving.
At least Rust has a chance to be largely correct because it has much greater effort per amount of code (in the compiler) invested into it than most any application code.
[flagged]
9 replies →
Rust’s type system enables the possibility of discovering and fixing a bug like this, and ruling out this class of bugs for all future programs.
The hand-waving comes from other languages which can’t do anything to prevent their users encounter such bugs and the ensuing CVEs.
I mean, Rust's whole shtick is safety, so that's really the only thing there is to "push" about the language.
I wouldn’t say so… I consistently choose Rust mainly because it’s a sanely designed modern C++ alternative. It’s 20% more effort than writing Python or Typescript, and you get to use the full power of your hardware without compromise.
Safety is a nice side-benefit. The main reason why I like the safety is because it allows you to fearlessly write high-level code without being constantly paranoid about memory as in C++. It’s more about enabling ergonomics without loosing performance, rather than security or correctness.
26 replies →
Idk, it also has a nicely expressive typesystem outside of lifetimes, a lot of modern syntactic features like pattern matching and monadic error handling, well-written compiler error messages, a well-designed standard library, and substantially less accrued cruft when compared to its largest competitor. Safety might be the cudgel its evangelists like to beat everyone over the head with, but there are certainly things to recommend it outside of that.
Rust has a lot of things that make it nice to write in. Robust enums and pattern matching are something I miss greatly when I’m back in C++. The trait inheritance system is also very flexible and I miss that. Especially compared to monstrosities like multiple inheritance.
Only people who don't write Rust think Rust's whole shtick is safety.
Consider reading past the hashtag.
Part of Rust's schtick is also cost free abstractions.
1 reply →
> not even Rust is free from hand waving.
It is moral though, so who cares really.
so what I take from this is that the rust compiler does not guarantee the stuff it claims to. Because new features of the type system is just being yolod instead of formally proven
EDIT: I said new features of the type system and more importantly, their interactions with the ever growing list of other features, not new features in the compiler. Totally different things. The compiler could be perfectly implementing the wrong choice of algorithms in the first place.
There never was formal verification of the entire rust compiler, or even its complete borrow checker/type system. There has been verifications on _subsets_ of them.
Also, a lot of those soundness issues aren't related to new features _at all_, but usually due to poor assumptions made in optimizations.
The soundness bugs _are_ taken seriously though, and are slowly being patched out. A lot of the links in OP are now closed because Rust either changed how it generates code to avoid the issues, or fixed LLVM.
https://github.com/model-checking/verify-rust-std
hm, there's an effort but scoped only to the std
It's terrifically complex: https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/ty...
not of the implementation. Of the type system. And a verification of subsets, but not a verification of their interactions == the whole system is unverified.
9 replies →
No mainstream compiler is formally proven. If you want a verified compiler, you pretty much have to choose between using a subset of standardml or a subset of C and the one proven compiler for each.
You're mistaking the semantics of the type system, from the implementation. I'm not talking about verifying the compiler. There's nothing to verify there.... literally. There is no spec to the language. By definition it is verified because the only verification you can do is tautological: "does this rust compiler do what this rust compiler does?"
But the unsoundness is because the type system itself, abstractly, was not verified. Or the interactions between parts. I.e. If you verified the compiler you'll find that it implements the algorithms perfectly. But tells you nothing about whether those implemented algorithms, however perfectly implemented, actually provided those guarantees.
2 replies →
Wait, there's a proven subset of C? Can you point me to some info?
3 replies →
There is a massive possibility space between “yolo” and formal proof. Rust has substantial evidence of correctness. For example, unit tests and types.
That's verifying the implementation. The type system wasn't verified. It implements stuff perfectly, it has tests that prove it, but nobody formally verified that they perfectly implemented the correct algorithms
4 replies →
[flagged]
25 replies →
Formal verification of the type system does seem a worthwhile goal, and to my understanding it's something the community has been making progress towards, but I also understand it's still relatively uncommon for most languages.
Is this more an abstract concern over the state of the industry, or is there a specific language you had in mind that you'd prefer Rust was modeled after?
Relatively uncommon as in there is not, as far as I know, a single mainstream language with a formally verified spec.
Important to note that this is is not a bug in the type system itself, it's a bug in the borrow checker not enforcing invariants that the type system says that it should, and formal verification of the type system would not have helped here.
The Java type system is also unsound. That’s life. It is hard to do this fully correctly. In practice this never comes up.
While true, there are two important differences:
1) Unsoundnesses in Java's type system are checked at runtime.
2) They (or at least some) are intentional or at least won't-fix bugs.
Both are not true for Rust.
The font color is so close to the background now that I can't even read your edit. Sorry, bud.
[flagged]
Yes. When people describe Rust as "a memory-safe programming language" they are describing an aspirational vision, and not a programming language that has actually been designed with sufficient rigor to guarantee memory safety. Any failure of rustc to actually guarantee this is just a bug in rustc itself, a failure to properly implement the Rust spec, because the closest thing Rust has to a spec is literally just the vague ideal that the compiler should guarantee safety somehow.
Rust cannot fail, it can only be failed.
I don't think the definition of "memory safe" has ever required full end to end stack conformance with a proof. Very few languages have achieved that, though some have. Most people call Java memory safe, C#, Python, Typescript, etc - all of those fall short of a formally verified, sound type system with a verified toolchain.
3 replies →
> Rust cannot fail, it can only be failed.
“Please build the perfect system. Because I specified ‘perfect’ any flaws are due to your incomplete implementation, not my awful brief.”
If the person writing the rust spec was a client I would have to drop them because they would be setting themselves up for dissatisfaction.
Would you say the same thing about Java? It’s type system is also unsound.
10 replies →
>Rust cannot fail, it can only be failed...
Sweet. But why should anyone care..