user since
Thu Nov 30 2000 at 19:59:04 (13.4 years ago )
last seen
Sun Feb 6 2005 at 22:23:12 (9.2 years ago )
number of write-ups
9 - View aleksey's writeups (feed)
level / experience
0 (Initiate) / 26
mission drive within everything
type safe programming languages
Stuy, Cornell, CMU
"Beware of bugs in the following code; I have only proved it correct, not tested it" -- Donald Knuth
most recent writeup
unique up to isomorphism
Send private message to aleksey

sleep! sleep!

I swear I didn't mean to stay up all night to node.

Just as you would no sooner build a cathedral using naught but a chisel, why do you write large systems in C?

The fundamental mistake of the average programmer lies in thinking of types as an obligation: my program must typecheck in order to appease the compiler. That is wrong. The compiler is there to help you, not the other way around. The blame lies not with the programmer, but with C (and C++, Java, Lisp, Perl and many of the others). The fact is that a more advanced type systems (as exemplified by ML and Haskell and by continued current research) are actually simpler to understand, lead to fewer mistakes and actively help the programmer in writing better code.

A type is a partial specification of correctness of an algorithm. And a program is a proof of that specification.

If you get this fundamental idea wrong, your should not continue in designing a programming language. Sadly, if you get this wrong, you join a large club where a lot of the members don't know that they are wrong.