Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Ada's dependent types, and its types as a whole

nytpu.com

Post reply on HN
Print view View original

51–60 of 146 posts

Re: Ada's dependent types, and its types as a whole

#51

Post by quietbritishjim »

LiamPowell wrote: post #24
quietbritishjim wrote: post #21

Earlier quoted context omitted.

> 2. Representation clauses almost entirely eliminate the need for the error-prone manual (de-)serialisation that's littered all over Linux driver code: Do representation clauses let you specify endianess? From a quick glance at that link it didn't appear so. I would imagine that invalidates most use cases for them.

You can specify endianness, but only over the entire record, not an individual field. The way it works is a little complicated: https://www.adacore.com/gems/gem-140-bridging-the-endianness...

Interesting, thank you. I think per-record is probably good enough for most applications, and less verbose than per-member. But it's not part of the language (that page calls it "implementation specific") and quite recent (that page is undated but references Ada 2012 so must be since then). It wouldn't have helped the Ada project I'm working on, which had an endianess crisis with serialisation a few decades ago.

Re: Ada's dependent types, and its types as a whole

#52

Post by pjmlp »

Keyframe wrote: post #42
seabird wrote: post #6

Ada is a criminally underrated tool that is unfortunately probably doomed to perpetually take the backseat to Rust despite Rust not solving all the problems Ada does. It's really sad that so many people's idea of safe programming is pretty strictly limited to memory safety, and that because Ada's baseline memory safety (SPARK is a different story) isn't as robust as Rust's borrow checker (in the sense that it doesn't…

Ada is a lot of fun and a great thing which is ruined (and blessed) by the fact there's de facto only one implementation and company behind it out in the open, and that is semi-closed / license PITA. There were improvements over the years by AdaCore, but I think this altogether hurt the adoption of such a great language in general - no other wide open implementation (like Rust has). If you want to see an extreme exam…

Not at all, there are 7 Ada compiler vendors still in business.

https://www.adacore.com/

https://www.ghs.com/products/ada_optimizing_compilers.html

https://www.ptc.com/en/products/developer-tools/apexada

https://www.ddci.com/products_score/

http://www.irvine.com/tech.html

http://www.ocsystems.com/w/index.php/OCS:PowerAda

http://www.rrsoftware.com/html/prodinf/janus95/j-ada95.htm

And AdaCore sponsors GNAT, with Ada being one of the few official GCC languages for two decades now.

Re: Ada's dependent types, and its types as a whole

#53

Post by Dylan16807 »

wffurr wrote: post #48
crabbone wrote: post #41

Earlier quoted context omitted.

I like Ada, but I tend to agree. "End Something_Somethig_Something" is really a mouthful (compared to "}"). And programmers are superficial like that. Ada wouldn't be the first decent language being dismissed for inconsequential aspects like this one.

Context free curly braces in deeply nested code make me crazy. Labels to match up with the open symbol would be super helpful. My company’s style guide requires them on closing braces for namespaces.

If you can't see the other end of a curly brace inside a function, I'm pretty tempted to say you're doing too much in one spot.

Re: Ada's dependent types, and its types as a whole

#54

Post by brabel »

touisteur wrote: post #38
jonlong wrote: post #15

Coming from the type theory side with only a passing glance at Ada, I am nevertheless sure: this is not what type theorists mean when they talk about dependently typed languages. Such languages derive from the formulation of Per Martin-Löf (also called Intuitionistic Type Theory), they include dependent sum and dependent product types, and they allow type checkers to prove complex statements about code. (The history…

SPARK allows you to statically prove properties about Ada code. Proving a sort implementation is a classic example : https://blog.adacore.com/i-cant-believe-that-i-can-prove-tha...

Looks really difficult to prove even a "hello world" algorithm. I'm afraid you can easily run into the problem of not understanding what you're proving and just not doing it for what you would actually want.

Re: Ada's dependent types, and its types as a whole

#55

Post by pjerem »

wffurr wrote: post #48
crabbone wrote: post #41

Earlier quoted context omitted.

I like Ada, but I tend to agree. "End Something_Somethig_Something" is really a mouthful (compared to "}"). And programmers are superficial like that. Ada wouldn't be the first decent language being dismissed for inconsequential aspects like this one.

Context free curly braces in deeply nested code make me crazy. Labels to match up with the open symbol would be super helpful. My company’s style guide requires them on closing braces for namespaces.

Let me say that I do agree with you.

However I’d add that this job could easily be done by the IDE. For a reason that I fail to grasp, after being around for multiple decades, IDEs are still incredibly bad at presenting useful information on the code. Apart from coloration and more recently type hints, there never have been any real innovation in just helping reading code structure. For some reason we are still stuck with a tree of files besides some glorified text editor.

Interestingly, we have made incredible progress into code comprehension. We have incredibly mature ast parsers, lsp servers, … our IDEs know everything about our code structure but we still fail to make anything else with that data than autocompletion and doc popups.

Re: Ada's dependent types, and its types as a whole

#56

Post by pjerem »

Dylan16807 wrote: post #53
wffurr wrote: post #48

Earlier quoted context omitted.

Context free curly braces in deeply nested code make me crazy. Labels to match up with the open symbol would be super helpful. My company’s style guide requires them on closing braces for namespaces.

If you can't see the other end of a curly brace inside a function, I'm pretty tempted to say you're doing too much in one spot.

In real life you’ll have to deal mostly with code you haven’t wrote yourself.

Re: Ada's dependent types, and its types as a whole

#57

Post by mirashii »

pjmlp wrote: post #52
Keyframe wrote: post #42

Earlier quoted context omitted.

Ada is a lot of fun and a great thing which is ruined (and blessed) by the fact there's de facto only one implementation and company behind it out in the open, and that is semi-closed / license PITA. There were improvements over the years by AdaCore, but I think this altogether hurt the adoption of such a great language in general - no other wide open implementation (like Rust has). If you want to see an extreme exam…

Not at all, there are 7 Ada compiler vendors still in business. https://www.adacore.com/ https://www.ghs.com/products/ada_optimizing_compilers.html https://www.ptc.com/en/products/developer-tools/apexada https://www.ddci.com/products_score/ http://www.irvine.com/tech.html http://www.ocsystems.com/w/index.php/OCS:PowerAda http://www.rrsoftware.com/html/prodinf/janus95/j-ada95.htm And AdaCore sponsors GNAT, with Ada be…

> out in the open

This part was an important part of the sentence you might've missed.

Re: Ada's dependent types, and its types as a whole

#58

Post by uticus »

LiamPowell wrote: post #47
typ wrote: post #40

Earlier quoted context omitted.

The popularity of a programming language is not always about what the language offers. I would say a comprehensive, well-documented, mature set of standard libraries for its target audience is far more important (notable examples like R, Python, and Go). Last time I checked, Ada doesn’t even have a de facto, high quality TLS/crypto library, let alone various essential protocol/format codecs, yet the core team (AdaCor…

There's some thick bindings to libtls that coincidentally happen to be written by the author of the article. There's also some OpenSSL bindings in Dmitry Kazakov's Simple Components and some in Ada Web Server by AdaCore, although they're pretty minimal. I think most applications of Ada are in embedded systems where you don't often want anything not in the standard library.

> I think most applications of Ada are in embedded systems...

Ada is heavily used and carries a historical influence not only with embedded software space, but also with hardware space: VHDL is one of the two major hardware description languages used in ASIC design and FPGA implementations. (The other language is Verilog, based on - you guessed it - C, because of its popularity.)

"Due to the Department of Defense requiring as much of the syntax as possible to be based on Ada, in order to avoid re-inventing concepts that had already been thoroughly tested in the development of Ada, VHDL borrows heavily from the Ada programming language in both concept and syntax." - https://en.wikipedia.org/wiki/VHDL#History

Re: Ada's dependent types, and its types as a whole

#59

Post by Ygg2 »

LiamPowell wrote: post #36
Ygg2 wrote: post #19

Earlier quoted context omitted.

> I'm a bit disappointed that we've ended up with Rust in the kernel but not Ada. Why? Do you program in Ada or Coq? People can't be bothered to track lifetimes, what makes you think they are ready to track pre/post-conditions, invariants and do it efficiently and thoroughly.

Having the option there is good, even if not everyone uses it. The same thing applies to Rust.

For Rust and Ada in the Kernel they need to be accepted by kernel maintainers.

And seeing they can't stand Rust, when its constraints are much weaker than Ada.Spark what chances does it have?

To paraphrase some computer science guru: The cyclical nature of programming languages is all to blame on the collective programmers. Rather than being guided by mathematic rigor, they are guided by a fashion sense.

Re: Ada's dependent types, and its types as a whole

#60

Post by adrian_b »

Dylan16807 wrote: post #53
wffurr wrote: post #48

Earlier quoted context omitted.

Context free curly braces in deeply nested code make me crazy. Labels to match up with the open symbol would be super helpful. My company’s style guide requires them on closing braces for namespaces.

If you can't see the other end of a curly brace inside a function, I'm pretty tempted to say you're doing too much in one spot.

Extracting sequences of statements into a function sometimes improves readability, when those sequences do together some recognizable operation, but other times such an extraction worsens a lot the readability, because now you need to also open other pages to see what the program really does, when the statements in a sequence are not really related.

Even in programs optimally written for readability it is frequent to have iterations or selection statements much bigger than a page, especially where the coding rules enforce a small length for program lines, e.g. 80 characters.

In languages that follow Algol 60, like Pascal, C, C++ and so on, which have a single kind of statement brackets, it is frequently needed to add comments on the final braces or "end", to avoid confusions when reading the program.

This is much more cumbersome than in the languages that follow Algol 68, e.g. Ada and bash, where there are several distinct pairs of statement brackets.

Post reply on HN