[throwaway729]

> How is this going to make my code better?

This blog post is describing a research agenda that has already provided tremendous fruit to language designers. You can find the echoes of this research agenda in the design and implementation of basically every modern typed language, as well as a lot of the infrastructure for dynamic languages.

If you're a language designer and you're not aware of the research agenda described in this blog post, learning more about programming language theory will be immensely beneficial.

If you're not a language designer, then your attitude is kinda weird and off-putting. Like demanding an explanation for how fluid mechanics will make your code better. (As it turns out, understanding the theory behind the languages you're using will make you a better programmer, but that's really beside the point.)

> As far as I remember attempts to use proofs in production were counter productive

You remember incorrectly.

> For most systems knowing that print "hello"; will do that is good enough.

Isn't this attitude exactly how we end up with vulnerability-riddled, brittle, and barely maintainable code? I can't think of a single system I've designed or implemented where all I needed to know was that STDOUT worked properly. Most of my test cases capture far more interesting properties. The more of those test cases my tooling can rule out for me, the better.

[posterboy]

> > As far as I remember attempts to use proofs in production were counter productive

Wait, does that mean in development? Otherwise, as I understood production so far it would be dependent typing. Supposedly that infers and automates a lot of otherwise handwritten safety checks.

> You remember incorrectly.

Indeed, Test Driven Development is huge and it's not even really formal. Formalisms should facilitate it a lot.

[hyperpape]

At some level of abstraction, types of any kind are already proofs, and they're tremendously important in many actual existing languages.

What you're probably glomming on to is that efforts to push the bounds of what you can prove (higher kinded or dependent types) have had mixed results (mixed in the sense that some people think they're great, others are unconvinced).

So we're in a weird situation where many many people are using a tool, but relatively few are interested in new developments concerning how to use that tool.

[throwaway729]

> Wait, does that mean in development?

I think xchaotic probably meant "in development of production code", and is wrong for two reasons:

1. Compilers are production code, and the research agenda this post describes informs a lot of that code (by way of language design). Unverified compilers still make a lot of use of underlying theory.

2. Correctness proofs and static analyses, which are both deeply related but different from what's being described in this post, are used in production environments every day.