logoalt Hacker News

mrkeen • today at 11:16 AM • 2 replies • view on HN

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.

Replies

vrighter • today at 11:58 AM

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.

➕ show 6 replies
codehero • today at 1:29 PM

"Type systems are hard!" As hard as its safety is pushed on us, not even Rust is free from hand waving.

➕ show 3 replies