Hacker News Reader

Fair, C may have been a better example. Where nearly everything is actually just a block of bytes of various lengths and can be intermingled fairly freely with minimal effort to get anything past the compiler.

Sometimes useful, but the type system ends up offering few meaningful protections as a consequence.

View on HN

The types of values and legal conversions between them are well defined in C -- the assumption that everything is just a block of bytes and hence may be casted freely between types is explicitly incorrect (and is what may lead to bad/invalid C code).

However, C does allow you to write code that can not proven to be legal with respect to the formal system of the language and get it to compile, I think that is what you are referring to.

But just because you can write an invalid program does not mean the type system doesn't exist or is flawed. I can also write an invalid Haskell program.

The difference between these two would be that the haskell program can be proven to contain only operations that map to well-defined operations in the formal language model by an automated process, while the same can not be done for C in the general case.

However, just because you can not always prove conformance to a formal model using automated means, doesn't mean that no formal model exists (because it does!).

Reply on news.ycombinator.com