Future proofed hipsters write in assembly and machine nowadays ;) Also don't for...

DanWaterworth · on March 22, 2013

Haskell is also rapidly becoming uncool. The cool kids use Coq, Agda or Idris.

bjterry · on March 22, 2013

Hilariously, there actually is an Agda web framework in development[1], although it seems like more of a research project than a serious effort. If there were a web framework in Coq, that would really be something. Idris is intended to be more general purpose, so hopefully one will be written someday.

For those not in the know, these are programming languages used mostly for developing mathematical proofs. They are all dependently-typed languages, which means that a type can depend on the values it contains. For example, you can constrain a function to only accept lists of a given length in a way that can be type-checked.

1: https://github.com/larrytheliquid/Lemmachine

DanWaterworth · on March 22, 2013

The vector type is always given as an example, but I find the ability to give a type to printf more mind bending.

Just in case that went over your head and to reiterate, that means that:

    printf "Hello %s" 4

would generate a type error, so would:

    printf "Hello %s" "wor" "ld!"

and:

    printf "Hello %s! %s" "world"

but:

    printf "%s %s!" "Hello" "world"

wouldn't.