5 ms·

Learning to love a rigid and inflexible language

86 points by tempodox 5y ago

AtlasBarfed 5y ago
"In the past I would have written this in C or Python" ... looks sideway at author.
hdkgjfhdj 5y ago
Ada, even with Spark, has formal verification capabilities that are nowhere near what has been achieved for C with Frama-C. With Frama-C you can prove that arbitrary heap allocated data structures with pointers are bug-free. You can’t do this with Ada Spark.
- jes 5y ago
  Link to a slide deck on Frama-C: https://cse.msu.edu/~cse814/Lectures/frama-c.pdf https://cse.msu.edu/~cse814/Lectures/frama-c.pdf
- nine_k 5y ago
  How much does Frama-C limit the ways you can write C code? How long does it take to check a reasonably sized code base?
- AlexCoventry 5y ago
  > you can prove that arbitrary heap allocated data structures with pointers are bug-free Can you say a bit more about that? The way that's written, it sounds like a solution to the halting problem.
  - curtisf 5y ago
    _Finding_ a proof is undecidable. _Verifying_ that a proof is correct is easy (it's usually linear-ish in the length of the proof). If the programmer supplies (most of) the proof, a compiler can easily certify that the proof is correct with respect to its model of the program. Still, constraint solvers (often SMT solvers) can succeed a lot of the time (just not _all_ of the time) in automating pieces of proofs, so all the tedium doesn't need to be left with the programmer. In particular, generally programmers write code that they believe is correct, so if they're right then there's usually a straightforward proof that it is correct since their beliefs will only get so complicated.
    - AlexCoventry 5y ago
      Ah, arbitrary heap-allocated structures a human can supply a proof for. Thanks; makes sense.
    - sterlind 5y ago
      my only experience in this area is Dafny, which aggressively automates the proof-finding (by passing it to Z3), but when that fails the compiler is exceedingly vague on what remaining obligations need to be discharged. You have to stumble around in the dark, trying asserts and assumes, until you narrow down where it got stumped. are there other automated-proof languages that do a better job on this?
flakiness 5y ago
TIL Part.1: QNX was acquired by BlackBerry at 2010 (and BB still is selling it!): https://en.wikipedia.org/wiki/QNX#History https://en.wikipedia.org/wiki/QNX#History TIL Part.2: SO covers Ada! [2]: https://stackoverflow.com/questions/tagged/ada https://stackoverflow.com/questions/tagged/ada This kind of random-looking, seriously-written but who-cares-other-than-few tech articles are something I'd love to read more.
- canadianfella 5y ago
  Why-do-you do-this?
- na85 5y ago
  QNX is why I'm bullish long term on Blackberry. They appear to be making a successful pivot, and they've got something like 90% of electric vehicle makers putting QNX in their cars.
  - foobiekr 5y ago
    I don't think this is a pivot at all. QNX in the nineties was a common embedded OS especially industrial.
    - na85 5y ago
      I mean that Blackberry is pivoting. They're not a phone company any more.
noengary 5y ago
I thought this might be about shopify's liquid madness
Jtsummers 5y ago
For anyone interested, the courses at [0] are good introductions to the language and its features. It's also nice to be able to run the code in the browser instead of having to install and configure everything on your own computer (nice for demos on the go, too). [0] https://learn.adacore.com/ https://learn.adacore.com/
the_only_law 5y ago
I love Ada, but sadly it probably missed its chance. There’s always the stories about how expensive the compilers were (and I think even now there’s some sort of weird license issues with GNAT and the Adacore tools) I have no interest working on legacy code at DoD contractors who are probably trying to replace it with C++ anyway. Some people have told me that companies like Nvidia had some Ada projects going, and I recall seeing some announcement, but never any jobs.
- ajxs 5y ago
  It depends where you are and what industry you're in. It's true that in some cases companies are trying to remove Ada from their codebase, however there's plenty of areas where Ada is dominant. Europe still has a large Ada presence in academia, and there's still plenty of new development using Ada in the transportation sector.
- inkyoto 5y ago
  > I love Ada, but sadly it probably missed its chance. There’s always the stories about how expensive the compilers were (and I think even now there’s some sort of weird license issues with GNAT and the Adacore tools) Not just Ada. There was a lot of buzz and excitement in mid- to late 90s about the design by contract paradigm (pre- and post-conditions, class invariants, generics, multiple inheritance done right, plus other nice things such as retriable and «self-healing» exceptions) and OOP that Bertrand Meyer had introduced with Eiffel and wrote a few books about. Sadly, nearly all languages have been relegated into oblivion or obscurity stemming from the proprietary nature of their respective compilers and development tools, which has entailed exorbitant costs of compilers and development toolchains. I was infatuated for a while with Sather, which was a Berkeley university open-source answer to Eiffel, however the language did not see any uptake in the development community and has succumbed to the same fate of other experimental languages. Ada has had pre- and post-conditions since day 1 (if my memory serves well), but the expensive compilers have relegated the language to fringe use cases as well. Even if at least a few of the design by contract ideas had gone mainstream (pre-, post-conditions, invariants at the very least), we would not have got carried away with the TDD now, writing unit tests verifying that 1 == 1 whilst allowing smart contracts to have farcical bugs. The rise of worse is better, ftw.

86 points by tempodox 5y ago

"In the past I would have written this in C or Python" ... looks sideway at author.

Ada, even with Spark, has formal verification capabilities that are nowhere near what has been achieved for C with Frama-C. With Frama-C you can prove that arbitrary heap allocated data structures with pointers are bug-free. You can’t do this with Ada Spark.

jes 5y ago
Link to a slide deck on Frama-C: https://cse.msu.edu/~cse814/Lectures/frama-c.pdf https://cse.msu.edu/~cse814/Lectures/frama-c.pdf
nine_k 5y ago
How much does Frama-C limit the ways you can write C code? How long does it take to check a reasonably sized code base?
AlexCoventry 5y ago
> you can prove that arbitrary heap allocated data structures with pointers are bug-free Can you say a bit more about that? The way that's written, it sounds like a solution to the halting problem.
- curtisf 5y ago
  _Finding_ a proof is undecidable. _Verifying_ that a proof is correct is easy (it's usually linear-ish in the length of the proof). If the programmer supplies (most of) the proof, a compiler can easily certify that the proof is correct with respect to its model of the program. Still, constraint solvers (often SMT solvers) can succeed a lot of the time (just not _all_ of the time) in automating pieces of proofs, so all the tedium doesn't need to be left with the programmer. In particular, generally programmers write code that they believe is correct, so if they're right then there's usually a straightforward proof that it is correct since their beliefs will only get so complicated.
  - AlexCoventry 5y ago
    Ah, arbitrary heap-allocated structures a human can supply a proof for. Thanks; makes sense.
  - sterlind 5y ago
    my only experience in this area is Dafny, which aggressively automates the proof-finding (by passing it to Z3), but when that fails the compiler is exceedingly vague on what remaining obligations need to be discharged. You have to stumble around in the dark, trying asserts and assumes, until you narrow down where it got stumped. are there other automated-proof languages that do a better job on this?

flakiness 5y ago

TIL Part.1: QNX was acquired by BlackBerry at 2010 (and BB still is selling it!): https://en.wikipedia.org/wiki/QNX#History https://en.wikipedia.org/wiki/QNX#History TIL Part.2: SO covers Ada! [2]: https://stackoverflow.com/questions/tagged/ada https://stackoverflow.com/questions/tagged/ada This kind of random-looking, seriously-written but who-cares-other-than-few tech articles are something I'd love to read more.

canadianfella 5y ago
Why-do-you do-this?
na85 5y ago
QNX is why I'm bullish long term on Blackberry. They appear to be making a successful pivot, and they've got something like 90% of electric vehicle makers putting QNX in their cars.
- foobiekr 5y ago
  I don't think this is a pivot at all. QNX in the nineties was a common embedded OS especially industrial.
  - na85 5y ago
    I mean that Blackberry is pivoting. They're not a phone company any more.

noengary 5y ago

I thought this might be about shopify's liquid madness

Jtsummers 5y ago

For anyone interested, the courses at [0] are good introductions to the language and its features. It's also nice to be able to run the code in the browser instead of having to install and configure everything on your own computer (nice for demos on the go, too). [0] https://learn.adacore.com/ https://learn.adacore.com/

the_only_law 5y ago

I love Ada, but sadly it probably missed its chance. There’s always the stories about how expensive the compilers were (and I think even now there’s some sort of weird license issues with GNAT and the Adacore tools) I have no interest working on legacy code at DoD contractors who are probably trying to replace it with C++ anyway. Some people have told me that companies like Nvidia had some Ada projects going, and I recall seeing some announcement, but never any jobs.

ajxs 5y ago
It depends where you are and what industry you're in. It's true that in some cases companies are trying to remove Ada from their codebase, however there's plenty of areas where Ada is dominant. Europe still has a large Ada presence in academia, and there's still plenty of new development using Ada in the transportation sector.
inkyoto 5y ago
> I love Ada, but sadly it probably missed its chance. There’s always the stories about how expensive the compilers were (and I think even now there’s some sort of weird license issues with GNAT and the Adacore tools) Not just Ada. There was a lot of buzz and excitement in mid- to late 90s about the design by contract paradigm (pre- and post-conditions, class invariants, generics, multiple inheritance done right, plus other nice things such as retriable and «self-healing» exceptions) and OOP that Bertrand Meyer had introduced with Eiffel and wrote a few books about. Sadly, nearly all languages have been relegated into oblivion or obscurity stemming from the proprietary nature of their respective compilers and development tools, which has entailed exorbitant costs of compilers and development toolchains. I was infatuated for a while with Sather, which was a Berkeley university open-source answer to Eiffel, however the language did not see any uptake in the development community and has succumbed to the same fate of other experimental languages. Ada has had pre- and post-conditions since day 1 (if my memory serves well), but the expensive compilers have relegated the language to fringe use cases as well. Even if at least a few of the design by contract ideas had gone mainstream (pre-, post-conditions, invariants at the very least), we would not have got carried away with the TDD now, writing unit tests verifying that 1 == 1 whilst allowing smart contracts to have farcical bugs. The rise of worse is better, ftw.