Hacker News Reader

Comment by mdup | Hacker News Reader

Before Rust, it could be said that Haskell has the same philosophy of ensuring almost everything works at compile-time.

Anyway, I hope for a future where programmers will be able to specify all contracts, invariants, etc. in code, and have them be checked upon compilation. And not only for "smart" programmers, but the pretty bad ones, too.

View on HN

>I hope for a future where programmers will be able to specify all contracts, invariants, etc. in code

Theoretically is this even possible? We simulate this with tests, and code-coverage analysis, but in the end all programs deal with unknown inputs, by definition.

There's certainly limits. Compilation-time type safety can only guarantee the absence of certain errors or presence of certain behaviours. Any question that can be reduced to the halting problem is something that cannot be automatically verified. However, there's lots of interesting and useful stuff that is not reducible to this problem. Such as "is this input really an integer?" (cough cough, dynamic languages)

This is a really old idea that does not increase productivity.

This is a really old idea that turned out to be harder than it looked, and require more computational power to be available to programmers than has generally been available. It has also required that this be available for long enough that it could build up a head of steam as people built up libraries that could be used to do real work and build runtimes that were strong in practice as well as theory.

Past failures can not always predict future failures properly in a Moore's Law regime. For instance, as everyone knows, tablet computing is a totally stupid and repeatedly failed idea, except, iPad. Computer vision is a complete waste of time, unless you have GPUs sitting around that can chew through billions of operations for cheap. Etc.

This "old idea" is getting somewhere now. It's only early days.

Reply on news.ycombinator.com