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

91–100 of 146 posts

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

#91

Post by docandrew »

brabel wrote: post #54
touisteur wrote: post #38

Earlier quoted context omitted.

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.

What’s nice is that you can do it in steps - you may have a hard time proving full specification, but you can prove absence of bad behavior like buffer overruns, etc and go from there.

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

#92

Post by Keyframe »

wavemode wrote: post #76
Keyframe wrote: post #64

Earlier quoted context omitted.

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.

Why would the license of the compiler matter? It doesn't require you to license the code you compile with it accordingly.

runtime matters

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

#93

Post by Keyframe »

debugnik wrote: post #89
Keyframe wrote: post #64

Earlier quoted context omitted.

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.

Haven't looked in a while. That's great news then! Rust steals a lot of thunder these days though.

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

#94

Post by DaiPlusPlus »

ajdude wrote: post #88
nytpu wrote: post #80

Earlier quoted context omitted.

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…

Your step 1 violated my very hard rule against piping curl into a shell.

…and is ironic advice for a safety-critical system, no?

——-

(Yes, I’ve read arp242.net/curl-to-sh.html - but my point being that as I’d be new to Ada then I don’t know who to trust; I’ve never heard of getada.dev therefore I don’t trust it)

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

#95

Post by pjmlp »

Agingcoder wrote: post #90
pjmlp wrote: post #52

Earlier quoted context omitted.

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 ?

A couple of them do, it isn't as if C and C++ FOSS compilers do as well.

https://en.cppreference.com/

C++23 and C23 are the latest, and there are plenty of missing features from previous standards.

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

#96

Post by debugnik »

crabbone wrote: post #41
zerr wrote: post #29

Earlier quoted context omitted.

The literally verbose syntax contributes to its unpopularity as well. It is extremely hard to skim/read and comprehend prose-like Ada code.

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.

End names are optional in Ada, so "fixing" that is just a style guide away. Meanwhile, Scala 3 added named `end` to help with long blocks on its indentation syntax.

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

#97

Post by ajdude »

DaiPlusPlus wrote: post #94
ajdude wrote: post #88

Earlier quoted context omitted.

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…

Your step 1 violated my very hard rule against piping curl into a shell. …and is ironic advice for a safety-critical system, no? ——- (Yes, I’ve read arp242.net/curl-to-sh.html - but my point being that as I’d be new to Ada then I don’t know who to trust; I’ve never heard of getada.dev therefore I don’t trust it)

It's an understandable rule, and you can definitely just download the binary from alire.ada.dev and add it to $PATH but with such a harsh stigma around how difficult it is to get the toolchain set up, GetAda follows the precedent of Rust, where you can grab the toolchain via "curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh" (thanks to Rustup).

It was received positively at the time:

Show HN: Getada: rustup-like installer for Ada's toolchain/package manager 194 points | 115 comments: https://news.ycombinator.com/item?id=40132373

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

#98

Post by throwup238 »

pjerem wrote: post #55
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.

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…

It’s called “sticky scroll” in VSCode and Visual Studio [1]. It pins the opening line of a scope to the top when it scrolls out of view and it does it multiple levels deep so you can see the class, function definition, conditionals, etc at the top of the source file when browsing deeply nested code.

[1] https://learn.microsoft.com/en-us/visualstudio/ide/editor-st...

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

#99

Post by docandrew »

4ad wrote: post #68

I am not versed in Ada, but Ada does not seem to have dependent types at all, in fact the author doesn't seem to understand what dependent types are. All his examples seem to revolve about arrays and bounded integers so I will stick to those example (although DT are far richer than that). In a language with dependent types you don't merely have arrays with arbitrary bounds, but you get a proof that array access is al…

One thing that’s kind of interesting about SPARK in particular - all the contracts get compiled to why3ml as an intermediate step before running through the solvers. If there are any VCs that can’t be discharged using the automatic provers, you can manually prove them using Coq: https://blog.adacore.com/using-coq-to-verify-spark-2014-code

I think the lines between what some consider true DT and what is possible w/ Ada might be more blurred than people expect.

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

#100

Post by com2kid »

zerr wrote: post #29
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…

The literally verbose syntax contributes to its unpopularity as well. It is extremely hard to skim/read and comprehend prose-like Ada code.

It was considered verbose years ago but now days it is IMHO better than messy C++ templates or Rust syntax.
Post reply on HN