alt Hacker NewsType 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
I wonder if TFA's example could be reproduced without mutability.
Replies
> Check out https://counterexamples.org/
A few past discussions if anyone is curious:
Counterexamples in type systems (2021) - https://news.ycombinator.com/item?id=48718972 - June 2026 (4 comments)
Counterexamples in Type Systems: programs that crash, segfault or explode (2021) - https://news.ycombinator.com/item?id=36213704 - June 2023 (97 comments)
Counterexamples in Type Systems - 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?
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.
"Type systems are hard!" As hard as its safety is pushed on us, not even Rust is free from hand waving.
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.