1. 32
  1.  

  2. 4

    Does anyone know why Ada is seeing a bit of a resurgence (at least, among the HN/Lobsters crowd)? I’m quite surprised by it, so I’m wondering if there are any interesting lessons that can be taken from it in terms of what causes languages to become popular.

    Also, what terms I should search for to find out more about Ada’s type system? It seems quite interesting - I’d love to learn more about what tradeoffs it’s making.

    1. 12

      Personally, after shunning Ada when I was younger because it felt cumbersome and ugly, I have seen enough failures where I’ve thought, “gee, those decisions Ada made more sense than I thought, for large projects”. I think some people are experiencing that; at the same time there’s this new wave of systems languages (often with stated goals like safety or being explicit about behavior) which is an opportunity for reflection on systems languages of the past; and SPARK is impressive and is part of the wave of new interest in more aggressive static verification.

      An earlier article posted on lobste.rs had some nice discussion of some interesting parts of Ada’s type system: http://www.electronicdesign.com/embedded-revolution/assessing-ada-language-audio-applications

      Also, the Ada concurrency model (tasks) is really interesting and feels, in retrospect, ahead of its time.

      1. 2

        I’m with you that it’s the new wave of systems languages that helped. The thing they were helping were people like me and pjmpl on HN that were dropping its name [among other old ones] on every one of those threads among others. There have been two, main memes demanding such a response: (a) the idea that Rust is the first, safe, systems language; (b) the idea that low-level, esp OS, software can’t be written in languages with a GC. There’s quite a few counters to the GC part but Burroughs MCP in ALGOL and Ada are main counters to first. To avoid dismissals, I was making sure to drop references such as Barnes Safe and Secure Ada book in every comment hoping people following along would try stuff or at least post other references.

        Many people contributing tidbits about the obscure systems languages on threads in a similar topic that had momentum. The Ada threads might be ripple effects of that.

        1. 3

          Now that I think about it, your posts are probably why I automatically associate Ada with Safe Computing these days.

      2. 7

        I think its part of the general trend of interest in formal methods and correctness (guarantees or evaluation of). We’ve also seen a lot on TLA+ recently, for example.

        1. 10

          I think lobsters, at least, is really swingy. A couple people interested in something can really overrepresent it here. For example, I either found or wrote the majority of the TLA+ articles posted here.

          And things propagate. I researched Eiffel and Design by Contract because of @nickpsecurity’s comments, which lead to me finding and writing a bunch of stuff on contract programming, which might end up interesting other people…

          One focused person can do a lot.

      3. 4

        In C you can mix an int and an int, but you can’t mix a struct serial_number and a struct port both of which contain an int.

        It’s easy enough to make an opaque type, and we can just as well sprinkle some assert in its implementation, for “bug traps.”

        I’d love to see more reasons for loving Ada, but I get a little tired of this “see we got types and C doesn’t” straw man. Evidently both languages have types and both languages provide a way to subvert the type system with unchecked conversions. Ostensibly, C programmers are not too keen on programming with a straight jacket, that’s why they keep mixing ints rather than turning every possible application of a numeric value to a new type.

        The other thing is, how far do you go with these types? Mixing up units is bad, but so is mixing different measurements (variables!) that use the same unit. Interior pressure vs exterior pressure? Both may be measured in bars, but get them confused, and you might just have a catastrophic accident ahead of you..

        Based on the few articles on Ada & Spark that I’ve seen, the way I imagine this kind of code would go is, well, you have function dealing with a variable exterior_pressure_bar. But you don’t trust yourself, so you also make it the type Exterior_Pressure_Bar. But you don’t trust your code once so you code the function again in a different language (Spark). Very redundant. Say the same thing thrice, maybe more than thrice, and maybe it will be correct… Perhaps appropriate for certain applications, but it doesn’t seem like much joy. Types are just one (relatively shallow) dimension of correctness, so focusing too heavily on that one part and introducing tons and tons of machinery to that end might just be a lot of work for little gain.

        I guess what I’m after is examples that are not so trivial. Yeah I know you can make types. And that you can write a function and a “proof” which says exactly the same thing the function’s body says, in slightly different words.

        The other thing I’d like to know is what features are there that actually save me typing (or just reduce bugs in some way that doesn’t require me to add more code or repeat myself saying I really really really mean to do this) and just make the code more readable overall? It seems that introducing such a maze of types and conversions is backfiring on readability & joy of writing department, so there’s got to be something to make up for it, no? And who checks that all the conversions I’m doing are the right thing to do? Maybe in that maze you’ll find code that converts interior pressure to bar to exterior pressure to mix them up.

        Admittedly the fixed point types are nice to have, and in C I’d prefer to have FP over the built-in complex type any day. Then again, it’s not terribly hard to implement your own fixed point code (or use one of the three billion existing implementations). Range types don’t seem too compelling; when was the last time I couldn’t decide which integer type was appropriate for my range? Now if they do overflow checking (in a way that isn’t more verbose than doing it in C), that’s a little better.

        1. 5

          Here are some reasons for not loving Ada:

          • It is not type safe, even if you only use features that were meant to be type safe. In other words, Ada’s type system fails at being a type system. “Almost safe” languages (Ada, Eiffel, etc.) are actually more dangerous than C, since at least C programmers are permanently aware that they are walking through a semantic minefield, whereas users of “almost safe” languages often think they aren’t.

          • Much of Ada’s type system exists to automate the insertion of runtime safety checks, just like much of pre-templates C++’s type system exists to automate the insertion of runtime type coercions and cleanup operations. Now, automation is nice, but, are types the right tool for this job? I do not think so. Macros offer a more compelling alternative.

          • With Ada, you can pick at most two between safety, efficiency and an implementation-independent semantics. Safely getting rid of the onerous runtime checks requires external analyses not evidently justified by the Ada specification. A formal semantics for the whole of Ada (not just the subset without dynamic resource management) is very much missing.

          1. 5

            at least C programmers are permanently aware that they are walking through a semantic minefield, whereas users of “almost safe” languages often think they aren’t.

            This is a very good point, and in my experience it also applies to functional purity. In an inherently impure language like C or Java, you’re always aware that shared mutable state is present and consequently you’re on guard for it, so you generally won’t build abstractions that depend on purity in order to work. In a language like Haskell or Elm, on the other hand, you know that the compiler actually offers strong purity guarantees at the type level, so you can use functional abstractions on a large scale with confidence. The real problem lies in the middle, when you’re using a language or a library that is pure by convention but will accept impure functions as well, and you build functional abstractions on it that break in really subtle and unexpected ways when mutability and nondeterminism come into play. I’d say an example of the latter category is some modern JS frameworks like React, which depend heavily on the programmer keeping track of what subset of their code has to be pure and what subset can be imperative, all in a language that has no compile-time ability to distinguish the two.

            1. 2

              It is not type safe, even if you only use features that were meant to be type safe. In other words, Ada’s type system fails at being a type system. “Almost safe” languages (Ada, Eiffel, etc.) are actually more dangerous than C, since at least C programmers are permanently aware that they are walking through a semantic minefield, whereas users of “almost safe” languages often think they aren’t.

              That example doesn’t support the point because it’s using an Unchecked package, which exist solely to side step the type system. They’re the Ada equivalents of Haskell’s Unsafe functions.

              Much of Ada’s type system exists to automate the insertion of runtime safety checks, just like much of pre-templates C++’s type system exists to automate the insertion of runtime type coercions and cleanup operations. Now, automation is nice, but, are types the right tool for this job? I do not think so. Macros offer a more compelling alternative.

              I don’t think I agree with the premise that Ada’s type system exists to automate the insertion of runtime safety checks. It can be viewed in that way, but so can any other type system. In reality, an Ada compiler is free to skip any runtime check that it can detect is unnecessary.

              1. 2

                That example doesn’t support the point because it’s using an Unchecked package, which exist solely to side step the type system.

                Re-read the code. The Conversion function doesn’t use anything from any Unchecked package. The Unchecked_Conversion function is only imported for comparison purposes.

                It can be viewed in that way, but so can any other type system.

                That would be wrong. For certain type systems, e.g. ML’s, it is a theorem that legal programs can be striped of all type information without altering the dynamic semantics of the language.

                In reality, an Ada compiler is free to skip any runtime check that it can detect is unnecessary.

                Yes, but it is in general undecidable whether a specific check can be safely elided. Things wouldn’t be so bad with a formal semantics for Ada, allowing programmers to verify by themselves that specific checks can be safely elided.

                EDIT: Fixed identifier. Added last sentence.

              2. 2

                I would like to add another reason: not much choice between implementations of Ada.

                1. 2

                  This one doesn’t bother me at all, although I can see why others would consider it a problem.

              3. 1

                What would be the best way to use ada for web development? Is there a cgi library?

                1. 1

                  People mainly used Ada Web Server from AdaCore. Googling on it also brought me to Ada Web Application. I think an easy project for someone interested in Ada would be porting one of the simpler, web frameworks from another language. Possibly modifying it as they go to use features specific to the new language for expressing the solution but otherwise keeping it the same. Then, they could port the plugins or libraries in its ecosystem one by one on top of new developments done natively.

                  1. 4

                    Ada on airplanes

                    1. 2

                      Yeah, the Boeing 777 team said they got all their programmers on Airplanes and that’s where’d they stay for 10-20 years. Makes more sense now.