Live data from Hacker News

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

nytpu.com

81–90 of 146 posts

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

#81
post #30

Earlier quoted context omitted.

Wouldn't Rust's symbol heavy syntax contribute the same?

I think that since a significant portion of Rust developers come from a C++ background, and C++ uses basically the same set of symbols, it's not a huge barrier to adoption

Rust actually has a bunch of oddities, to the point they test them [0].

[0] https://github.com/rust-lang/rust/blob/master/tests/ui/weird...

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

#82
post #81

Earlier quoted context omitted.

I think that since a significant portion of Rust developers come from a C++ background, and C++ uses basically the same set of symbols, it's not a huge barrier to adoption

Rust actually has a bunch of oddities, to the point they test them [0]. [0] https://github.com/rust-lang/rust/blob/master/tests/ui/weird...

There's really only one sigil in there that isn't in C++ (the ' single-quote to name lifetimes and labels). And it's missing several ambiguities that plague older C++ grammars (i.e. is >> a greater than, or closing two template expressions?)

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

#83
post #77

Earlier quoted context omitted.

> you get a proof that array access is always within bounds But the way you get 'proofs' in dependently-typed languages is just by building a tree of function evaluations that demonstrate a given logical inference at compile time, and that disappear (are translated to a unit type) when 'program extraction' is performed on the code. This is ultimately a kind of meta-programming. And in a DT language you would still ne…

> This is ultimately a kind of meta-programming. There is connection between advanced type systems and metaprogramming, you don't even need dependent types to reach it, GHC can express, for example, typed symbolic differentiation of compiled terms[1], something that would be of interest to a Lisp programmer. This is not a surprise, System Fω has a copy of simply typed lambda calculus at the type level. > But the way…

> Programs in most DT languages run directly (Lean, Idris, Adga, etc), code extraction is a Coq thing (and Isabelle, but Isabelle does not use DT). Some languages have type erasure, some don't. Some are explicitely concerned about type erasure (Idris), some don't.

Lean has proof irrelevance which means that any information that may be contained within the "proof" or "logical" part of the program is erased at runtime. It amounts to largely the same thing.

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

#84
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.

Agreed but it’s not always my own code I am reading.

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

#85

Earlier quoted context omitted.

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.

Ada 95 added bit ordering.

https://www.adaic.org/resources/add_content/standards/95rat/...

https://www.adaic.org/resources/add_content/standards/95lrm/...

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

#86
post #40
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…

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…

Very few of which are needed or even wanted for lower level mcu development. I assume when the gp was talking about spinning things they were talking about ESC software.

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

#87
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…

Yeah, to this day Ada, though a beautiful language, is a hard choice to make if you are concerned about certain targets. How would i get my program to compile to Android NDK? Even Swift has a better story with it's tooling.

That's before we even talk about important stuff like libraries.

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

#88
post #80

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…

It's FOSS and is actually included with GCC, but the toolchain is still a PITA to install just because no one (other than Debian and Arch Linux) bothers packaging it. I think Alire is supposed to make it easy to install but I haven't used it much: https://alire.ada.dev/ SPARK 2014 itself is the same too AFAIK, the problem is there's a lot of auxiliary static analysis tools and plugins that are gated behind AdaCore's…

The situation was pretty bad a few years ago, and the licensing was confusing but it's pretty straightforward now with Alire. (AdaCore also got rid of their "Community Edition which had the weird license restrictions).

I'm doing a presentation at FOSDEM next year called "Get started with Ada in 2 minutes or less!"[1]; because (on MacOS and Linux) I can go from not having no toolchain a all to compiling hello world in under 2 minutes (I've timed it).

Here's some steps:

1. open your terminal, run the following command: curl --proto '=https' -sSf https://www.getada.dev/init.sh | sh

Congratulations, you now have Alire!

2. Run the following command: alr init --bin hello

Now you have a fully structured Ada project, gpr files and all!

3. Edit your program in hello/src/hello.adb

You can use vscode to open the hello folder with the Ada Language server, or just run "alr edit" to open your editor with all of the files built in.

4. Compile with: alr build

Alire will automatically grab the latest native toolchain (gnat, gprbuild, etc) and compile the program.

If you want to use another toolchain, such as for cross-compiling, or another version of GNAT, simply run: alr toolchains --select

5. Run the program: hello/bin/helo

On windows, you can just download the windows installer; alire is also on Freshports for the BSDs.

[1] https://fosdem.org/2025/schedule/event/fosdem-2025-5056-get-...

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

#89

Earlier quoted context omitted.

As far as I'm aware, the compiler AdaCore sells is just GCC. You can install GCC built with Ada support from your distros package manager and it will just work. You can also download builds from here: https://github.com/alire-project/GNAT-FSF-builds

If something hasn't changed, FSF builds are a year behind libre version (by design), and libre version is GPL3 cancer which is not suitable for commercial development. You're then stuck either with a year old version or buy into AdaCore Pro version of it. Not great, not terrible.. but that's kind of the only game out in the open, which is what makes it different from most of other languages out there.

GNAT CE isn't a thing anymore, only FSF and Pro exist. And AdaCore now sponsors Alire, which installs FSF GNAT, and relicensed some of their tools more permissively.

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

#90
post #52

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…

Do they all support the latest standards ?
Post reply on HN