logoalt Hacker News

ameliusyesterday at 11:01 PM2 repliesview on HN

Yeah we don't throw programming languages away because they are undecidable.

So why would we throw type systems away if they are undecidable?


Replies

ChadNauseamyesterday at 11:04 PM

Decidability isn't even that useful. If typechecking takes a million years, that's also bad. What you want is guarantees that correct programs typecheck quickly. Without this, you end up in swift land, where you can write correct code that can't be typechecked quickly and the compiler has to choose between being slow or rejecting your code

show 1 reply
BalinKingtoday at 12:44 AM

My 2¢ from an interactive theorem proving perspective: In so-called computational type theory, typechecking is indeed allowed to be undecidable, and you get a lot of cool expressive power (e.g. well-behaved quotients and subtypes) as a result. This was one of the big ideas behind NuPRL back in the day, and Istari[0] more recently.

[0] www.istarilogic.org