3 ms·

Dying breed based on what? They're different compromises, there is nothing inherently superior about static types. It's more popular right now, because we're ve

Dying breed based on what? They're different compromises, there is nothing inherently superior about static types. It's more popular right now, because we're very much into rules at the moment; but I have a feeling that's peaking. Typically, you need to move back and forth a number of times before it clicks. So you have all these people on the net fighting over which end of the spectrum is the Right one, and next month they're on opposite sides. They're tools, hammers, screw drivers whatever; it doesn't make any kind of sense to identify with them. Unless your goal is to be a tool, I guess.

nickpsecurity 8y ago
There is one advantage of formal specs in general that static types inherent: they can enforce a correctness policy on a design that works for all inputs with no runtime overhead. SPARK Ada eliminating entire classes of errors with mostly-automated analysis is one example. Rust blocking temporal and some concurrency errors without GC is another. I'll note they're both hard to eliminate with testing, too. With that, comes the next benefit: less debugging and lower maintenance costs. It has to be balanced against annotation costs. Most projects claimed to come out ahead if it was just safety rather than full correctness. You can also generate tests and runtime checks from specs to get those benefits. So, for high reliability with lower maintenance, there's definitely an advantage to knocking out entire classes of error. That leads to last advantage Ill mention: ability to warranty (market) and certify (regulators) your code free of those defects [if the checker worked]. The checkers are also tiny on some systems. Rarely fail. Inspires extra confidence.
- sifoobar 8y ago
  Sure, in return for bending code over backwards to fit rules you get guarantees; but pretending that is anything but a different compromise isn't helping. If Ada was all that, everyone would be using it; and that's not going to happen, because it's not a realistic approach to programming. The academic approach doesn't look very constructive to me, never did. Once you have a language nailed down so hard that errors aren't possible, the complexity of dealing with it will be more or less the same as dealing with the errors in the first place. I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety.
  - nickpsecurity 8y ago
    "If Ada was all that, everyone would be using it" Argument for popularity = superiority. By your same logic, we shouldve stuck with COBOL for important apps since all the big businesses were using it. I have a feeling you dont write new apps in COBOL. "the complexity of dealing with it will be more or less the same as dealing with the errors in the first place." The best empirical comparison of C and Ada showed the opposite. All studies showed the safer languages had less defects with usually more productivity due to less rework later on. Evidence is against your claim so far. "I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety." Me too. Rust and Nim are taking that approach. People are finding both useful in production so far.
olodus 8y ago
Wow wow chill out. It wasn't meant as a negative comment. I was just making the observation most new languages are staticly typed and that a lot of what you hear in the functional space is about types (type theory, dependant types, categories...) though this might be just what I've had infront of me recently. I retract my statement. I love the dynamic functional languages. Erlang and Clojure are amazing (now that I think about it elixir is a lot in the news, as I said my statement probably was wrong). And as I said in my previous comment, I think Rich talk made some really interesting points.
olodus 8y ago
And I don't consider clojure dying at all btw. In the field of data science especially it is thriving. I was tired ok... So... There...

nickpsecurity 8y ago

There is one advantage of formal specs in general that static types inherent: they can enforce a correctness policy on a design that works for all inputs with no runtime overhead. SPARK Ada eliminating entire classes of errors with mostly-automated analysis is one example. Rust blocking temporal and some concurrency errors without GC is another. I'll note they're both hard to eliminate with testing, too. With that, comes the next benefit: less debugging and lower maintenance costs. It has to be balanced against annotation costs. Most projects claimed to come out ahead if it was just safety rather than full correctness. You can also generate tests and runtime checks from specs to get those benefits. So, for high reliability with lower maintenance, there's definitely an advantage to knocking out entire classes of error. That leads to last advantage Ill mention: ability to warranty (market) and certify (regulators) your code free of those defects [if the checker worked]. The checkers are also tiny on some systems. Rarely fail. Inspires extra confidence.

sifoobar 8y ago
Sure, in return for bending code over backwards to fit rules you get guarantees; but pretending that is anything but a different compromise isn't helping. If Ada was all that, everyone would be using it; and that's not going to happen, because it's not a realistic approach to programming. The academic approach doesn't look very constructive to me, never did. Once you have a language nailed down so hard that errors aren't possible, the complexity of dealing with it will be more or less the same as dealing with the errors in the first place. I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety.
- nickpsecurity 8y ago
  "If Ada was all that, everyone would be using it" Argument for popularity = superiority. By your same logic, we shouldve stuck with COBOL for important apps since all the big businesses were using it. I have a feeling you dont write new apps in COBOL. "the complexity of dealing with it will be more or less the same as dealing with the errors in the first place." The best empirical comparison of C and Ada showed the opposite. All studies showed the safer languages had less defects with usually more productivity due to less rework later on. Evidence is against your claim so far. "I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety." Me too. Rust and Nim are taking that approach. People are finding both useful in production so far.

olodus 8y ago

Wow wow chill out. It wasn't meant as a negative comment. I was just making the observation most new languages are staticly typed and that a lot of what you hear in the functional space is about types (type theory, dependant types, categories...) though this might be just what I've had infront of me recently. I retract my statement. I love the dynamic functional languages. Erlang and Clojure are amazing (now that I think about it elixir is a lot in the news, as I said my statement probably was wrong). And as I said in my previous comment, I think Rich talk made some really interesting points.

olodus 8y ago

And I don't consider clojure dying at all btw. In the field of data science especially it is thriving. I was tired ok... So... There...