2 ms·

I remember reading the first entry many years ago and wondering why anyone would want to use a language with type enforcement when you could have duck typing. (

by schoen 7y ago

I remember reading the first entry many years ago and wondering why anyone would want to use a language with type enforcement when you could have duck typing. (I thought of types as something that had been enforced by the lack of expressive power of old languages in which the types were effectively closer to the machine -- like describing the size of a machine word or something.) Later on I experienced the famous feature of Haskell in which it takes a while to write a valid program that compiles at all, but then the program immediately works correctly the first time and is free of several large classes of bugs. So yeah, excellent description of that trend! Edit: another closely related phenomenon is people gaining a new appreciation for formal grammars and formal specifications, understanding how hard parsing problems are and how bad the consequences of underspecification and undefined behavior can be. I imagine in the Jargon File heyday it would have been made fun of to use formal specifications everywhere, but now some of the most successful systems and tools use them to good effect. Maybe there was a "formal methods winter" or "formalism winter" to parallel the AI Winter? Edit 2: also, as a sibling comment mentions, these tools are much nicer to use now than they were then. Protobuf and friends do something akin to what ASN.1 did, but the tools around them are so much nicer!

Gibbon1 7y ago
My limited experience with dynamic languages vs the more persnickety typed languages is with the former you really really really need unit testing. I found the more type enforcement the less bugs of the sort unit tests catch. I wonder what programmers of that era would have thought is their introduction to dynamic languages was in an environment heavy on TDD and unit tests. Likely not so fond.
kragen 7y ago
Yes, I think there was very much a "formal methods winter", say from about 1985 to 2015; the Jargon File alludes to this in the "DWIM" entry, I think. Essentially, proving tiny programs correct became feasible in the mid-1960s, but only tiny programs were feasible to prove correct until the mid-oughts. Dijkstra died terribly disappointed. During essentially this entire time period, the scale of what people were programming was growing much faster than the scale of what people could prove correct. If the aspirational task in 1995 was to prove correct a telecom switching system, the aspirational task in 2005 was to prove correct an AJAX frontend in untyped JS with its goofy coercion rules speaking over an unreliable network with MITM proxies to a backend written in untyped PHP, storing its data in a MySQL cluster where it would read from a read slave that was different from (and a poorly characterized latency period behind) the master it was writing to. Since then things have gotten more complicated, but I feel that formal methods have closed a bit of the gap. However, I don't think of Ada as being a promising part of these developments. It isn't especially formally tractable, and it doesn't even attempt to offer the kinds of safety guarantees that Rust does. Rust, CompCert, seL4, Z3, Haskell, OCaml, and TLA+ seem a lot more promising than Ada. Heck, even Hypothesis is kind of in that category for me. P.S. I miss you. I hope you're doing well.

by schoen 7y ago

Gibbon1 7y ago

My limited experience with dynamic languages vs the more persnickety typed languages is with the former you really really really need unit testing. I found the more type enforcement the less bugs of the sort unit tests catch. I wonder what programmers of that era would have thought is their introduction to dynamic languages was in an environment heavy on TDD and unit tests. Likely not so fond.

kragen 7y ago

Yes, I think there was very much a "formal methods winter", say from about 1985 to 2015; the Jargon File alludes to this in the "DWIM" entry, I think. Essentially, proving tiny programs correct became feasible in the mid-1960s, but only tiny programs were feasible to prove correct until the mid-oughts. Dijkstra died terribly disappointed. During essentially this entire time period, the scale of what people were programming was growing much faster than the scale of what people could prove correct. If the aspirational task in 1995 was to prove correct a telecom switching system, the aspirational task in 2005 was to prove correct an AJAX frontend in untyped JS with its goofy coercion rules speaking over an unreliable network with MITM proxies to a backend written in untyped PHP, storing its data in a MySQL cluster where it would read from a read slave that was different from (and a poorly characterized latency period behind) the master it was writing to. Since then things have gotten more complicated, but I feel that formal methods have closed a bit of the gap. However, I don't think of Ada as being a promising part of these developments. It isn't especially formally tractable, and it doesn't even attempt to offer the kinds of safety guarantees that Rust does. Rust, CompCert, seL4, Z3, Haskell, OCaml, and TLA+ seem a lot more promising than Ada. Heck, even Hypothesis is kind of in that category for me. P.S. I miss you. I hope you're doing well.