Dynamic vs Static Languages

Elben Shira’s thoughtprovoking The End of Dynamic Languages inspired many wonderful responses, for example Have Static Languages Won?, What Consitutes Winning, and The Sky Is Not Falling.

If Elben is offering odds then I will absolutely put money a new successful dynamic programming language for 3 reasons:

  1. Most programmers don’t start in a language with a powerful static type system. Organically these programmers seek the expression and creativity dynamic languages provide. Only after experiencing some malevolent runtime bugs will they seek out the safety of powerful type systems.

  2. Not all problems require static typing. To @Yoghos’s point, we correctly seek out languages that concisely express the solution. We need static typing in shell scripting languages and I’m sure a new one will come along at some point to replace Bash.

  3. Even if statically typed languages are the messiah, the discerning bettor must take the side of a single successful dynamic language appearing between now and the end of time.

A more serious question:

Can we prove program correctness without static typing?

Yes: we can use a Formal Specification Language. Oh boy, but that looks much more complicated than using a powerful static type system …​ and there are few tools to help us translate formal specifications to a programming language we can use. Ah. We have a short cut! Property Testing! Property Testing allows us to build a formal functional specification of our programs, proving them correct without the need of a Formal Specification Language. Benjamin Pierce’s keynote A Deep specification for Dropbox from Clojure/Conj 2105 delves deeper into Formal Specification and Property Testing for correctness.

November 29, 2015
Tags: dynamic static languages clojure-conj-2015