Conversation

Hi, resident "type systems are way overhyped" thought leader here. This argument misrepresents the value of type systems and correctness techniques in general. Verification is designed to help, not solve everything, and it's designed to be used in defense-in-depth. twitter.com/devoncestes/st

This Tweet is unavailable.

193

Ken and 69 others

@piq9117

Jun 10, 2020

Man expects type checker to understand his function name.

Hillel

@hillelogram

Jun 10, 2020

I think that's being a little bit unfair to him

vilem

@buggymcbugfix

Jun 10, 2020

Huh, this is what I understand too.

Hillel

@hillelogram

Jun 10, 2020

I read it more as "the kinds of errors I care about are the kinds of errors type checkers can't solve, or even should solve"

David Justo

@davidjustodavid

Jun 10, 2020

While I realize this is besides the point, I'm under the impression that you could solve this via refinement types and some lightweight annotations. Is that wrong?

Replying to

There was a follow-up comment in the thread that brought up refinement types, and then the OP responded by bringing up the issue of buggy specifications.

11:06 PM · Jun 10, 2020Twitter Web App

Likes