~bfiedler/website

70e2b7b029db5e9806e97c6aba66274fa49e0ed2 — Ben Fiedler 3 months ago bbf3589
Link to Rust unsoundness issue

Fixes #15
1 files changed, 1 insertions(+), 1 deletions(-)

M static/typing-is-hard.html
M static/typing-is-hard.html => static/typing-is-hard.html +1 -1
@@ 93,7 93,7 @@
<h3 id="ml">ML</h3>
<p><strong>decidable</strong>, uses Hindley-Milner</p>
<h3 id="rust">Rust</h3>
<p><strong>undecidable</strong>, both type inference (since Rust has rank-3-types) and type checking, as shown by this <a href="https://sdleffler.github.io/RustTypeSystemTuringComplete/">Smallfuck interpreter implemented using traits</a>.</p>
<p><strong>undecidable, unsound</strong>, both type inference (since Rust has rank-3-types) and type checking, as shown by this <a href="https://sdleffler.github.io/RustTypeSystemTuringComplete/">Smallfuck interpreter implemented using traits</a>. There is a long-standing (open since 2015) bug about an <a href="https://github.com/rust-lang/rust/issues/25860">unsoundness issue with traits</a>.</p>
<h3 id="scala">Scala</h3>
<p><strong>undecidable</strong>, since it admits a <a href="https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/">type-level SKI calculus</a>, <strong>unsound</strong>, as shown by <a href="https://dl.acm.org/doi/pdf/10.1145/2983990.2984004">Amin and Tate (2015)</a>. Scala 2.13.3 (newest as of writing this) also exhibits the same problem.</p>
<h3 id="swift">Swift</h3>