Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Static Typing is not enough

blog.fogus.me

Post reply on HN
Print view View original

1–10 of 65 posts

Re: Static Typing is not enough

#2

Post by carsongross »

Neither static typing (nor any of the other stuff mentioned) is enough to ensure correctness. Never has been, never will be.

However, static typing is enough for some sweet, sweet hit-dot-wtf-can-i-do-completion-refactoring-like-a-boss tooling goodness.

Re: Static Typing is not enough

#3

Post by fogus »

carsongross wrote: post #2

Neither static typing (nor any of the other stuff mentioned) is enough to ensure correctness. Never has been, never will be. However, static typing is enough for some sweet, sweet hit-dot-wtf-can-i-do-completion-refactoring-like-a-boss tooling goodness.

    (any of the other stuff mentioned) .. ensure correctness
The post says that.

Dot-completion in your IDE is not enough either, nor is it something particularly unique to static languages.

Re: Static Typing is not enough

#4

Post by tomp »

Sometimes, I wish I could downvote stories...

Accidentially, almost everything that the author suggests, except luck and user testing, can be provided by static type systems - e.g. Haskell's type system is Turing-complete, so you can make up any kind of contracts/tests and embed them into the type system...

Re: Static Typing is not enough

#5

Post by chipsy »

This is as much a usability problem as it is a "getting it right" one. We could eventually "get it right" by plugging in raw machine code through switches or punchcards if that's really what it took, but what we're arguing over is the _price_ of getting it right.

Static types are implemented and available for use at the language level, which isn't true of all of those features in most environments.

Re: Static Typing is not enough

#8

Post by roryokane »

fogus wrote: post #3
carsongross wrote: post #2

Neither static typing (nor any of the other stuff mentioned) is enough to ensure correctness. Never has been, never will be. However, static typing is enough for some sweet, sweet hit-dot-wtf-can-i-do-completion-refactoring-like-a-boss tooling goodness.

(any of the other stuff mentioned) .. ensure correctness The post says that. Dot-completion in your IDE is not enough either, nor is it something particularly unique to static languages.

> The post says that.

I think the grandparent knew that, and was just repeating what you said to contrast it with his following statement about what static typing is good for.

And dot-completion is not completely unique to static languages, but I would say it is “particularly unique” – it is more common for static languages. And that’s not just coincidence – it is generally easier to write a tool like dot-completion for a static language than a dynamic language, because dot-completion involves static analysis of the code.

Re: Static Typing is not enough

#9

Post by jerf »

tomp wrote: post #4

Sometimes, I wish I could downvote stories... Accidentially, almost everything that the author suggests, except luck and user testing, can be provided by static type systems - e.g. Haskell's type system is Turing-complete, so you can make up any kind of contracts/tests and embed them into the type system...

With appropriate compiler flags, you can make up any sort of contracts you like in Haskell. But there's no guarantee that the compilation process will terminate if you do, even putting aside the impenetrability of the resulting code. Haskell is not a general purpose proof assistant, and the typing definitely has limits both practical and theoretical. Abstractly, static types can represent anything, however we (by which I mean humanity in general) certainly do not know how to use such powerful types in real, general purpose code.

If you want to go that road, look up Agda or Coq.

Post reply on HN