Further to the previous post. The talk on Hazel is fascinating.
I’ve been thinking for a while about the importance of being able to program “in your own order” ie. fill the blanks of your decision making about your program as and when you have that information available to you / or as you feel like tackling that problem. And leaving the undecideds and unknowns until later.
Holes in Hazel and other theorem provers offer that capacity in the small. And obviously tied to some advanced type theory which is a bit beyond me, but I think I grok the basic ideas. And, yes, having a formalization of the unknowns is a powerful idea.
A comment I made over on The End of Dynamic Languages
The problem with the static / dynamic debate is that the problems / costs appear in different places.
In static languages, the compiler is a gatekeeper. Code that gets past the gatekeeper is almost certainly less buggy than code that doesn’t get past the gatekeeper. So if you count bugs in production code, you’ll find fewer in statically typed languages.
But in static languages less code makes it past the compiler in the first place. Anecdotally, I’ve abandoned more “let’s just try this to see if its useful” experiments in Haskell where I fought the compiler and lost, than in Clojure, where the compiler is more lenient. (Which has the knock on effect of my trying fewer experiments in Haskell in the first place, and writing more Clojure overall.)
Static typing ensures that certain code runs correctly 100% of the time, or not at all.
But sometimes it’s acceptable for code to run 90% of the time, and to have a secondary system compensate for the 10% when it fails. There might even be cases where 90% failure and 10% success can still be useful. But only dynamic languages give you access to this space of “half-programs” that “work ok, most of the time”. Static languages lock you out of it entirely. They oblige you to deal correctly with all the edge cases.
Now that’s very good, you’ve dealt with the edge cases. But what if there’s an edge case that turns up extremely rarely, but costs three months of programmer time to fix. In a nuclear power station, that’s crucial. On a bog-standard commercial web-site, that’s something that can safely be put off until next year or the year after. But a static language won’t allow you that flexibility.
The costs of static and dynamic languages turn up in different places. Which is why empirical comparisons are still hard.
The magic of Functional Programming is that you can write the verbs before the nouns.
You have so little commitment to what the data structures are, that it doesn’t get in the way.
Today I find myself mapping across and diff-ing lists of arbitrary ad-hoc dictionaries and tuples.
Had I sat down and had to invent / write methods in terms of classes or Haskell’s parameterized types I’d never have thought of these ad-hoc collections as types to define methods on or even to define functions in terms of.
But as it is, mid-function, I can just decide that what I need is to put them into a collection and process this collection in some way.