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

101–110 of 146 posts

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

#101

Post by pyjarrett »

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.

About two years ago, I was able to dive into the Ada reference manual formatter which has initial commit of March 2000 and is about 45k lines of code, and add MDX output pretty easily.

Other languages focus on terseness and expressiveness. Ada expresses a bunch of constraints directly and forces you to do things in organized ways (e.g. use namespaces appropriately).

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

#102

Post by samatman »

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)

Is it really so bad to run it twice, with cat/bat replaced with sh on the second pass? If you're really paranoid about it you could save the first run to a file, so you know for certain that the server didn't do a switcheroo for the second one, but if you think about it, that's a low-payout move for Bad Guy #N compared to just sending the pwnage the first time around.

This is beside the fact that we're talking about downloading and running a user-owned binary, which, unlike the shell script, is impractical to inspect in any detail, and has the same privileges as the shell script we're supposed to worry about.

I view "don't curl to shell" as about 90% theatrics basically. Sure, read it first, I do in fact do that. But it's a silly 'very hard rule'.

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

#103

Post by jerf »

samatman wrote: post #102
DaiPlusPlus wrote: post #94

Earlier quoted context omitted.

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)

Is it really so bad to run it twice, with cat/bat replaced with sh on the second pass? If you're really paranoid about it you could save the first run to a file, so you know for certain that the server didn't do a switcheroo for the second one, but if you think about it, that's a low-payout move for Bad Guy #N compared to just sending the pwnage the first time around. This is beside the fact that we're talking about…

I routinely save to a file before execution, but it's not really about being attacked. It's about the fact that those scripts, in order to be "fire and forget", make many assumptions, often very large ones, about where I want things or under what user, etc.

Many of them are actually quite well-written under the hood and can be easily moved to other directories, have comments about what it is doing, etc.

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

#104

Post by Yoric »

zozbot234 wrote: post #45
Yoric wrote: post #37

Earlier quoted context omitted.

For what it's worth, many Rust developers (including myself) are also Ada fans. Note that ranged types, decimal types, etc. can fairly easily be emulated in Rust, with what I find is a clearer error mechanism. SPARK is, of course, extremely cool :) There are several ways to work with theorem provers and/or model checkers in Rust, but nothing as nicely integrated as SPARK so far.

I would quibble with the "fairly easily" part. It will likely become possible to make them as ergonomic as the Ada variety if Rust's const generic and constant evaluation facilities are extended far enough, but this would also open up the can of worms of essentially giving Rust the full capabilities of a dependently-typed language (at least in its compile-time subset), which Rust's dev community may not necessarily b…

I'll grant you that Rust is not nearly as ergonomic as Ada in this domain, but doing it manually is fairly easy. Turning it into a library is a bit more complicated - these days, I'd do it with macros. Of course, making sure that the compiler knows about it for optimization purposes would require lots of const generic.

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

#105

Post by crabbone »

debugnik wrote: post #96
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.

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.

Like in all such discussions: the problem isn't with what you write, but with what you read. There are tons of Ada code that's already written like that. So, future changes to the style guide aren't going to do much. Also, nobody's changing that anyways.

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

#106

Post by crabbone »

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.

So, this is a problem with using good editors. I don't know if VSCode or any similar editors have the way to select current block / current function, but in Emacs (and mostly likely Vi(m)) world this is just part of knowing the ropes. So, giving extra emphasis to the end of the function (or block) is completely unnecessary, it just reduces entropy.

Other problems with this: one of the ways to navigate the code is by searching for the function (procedure) name. Now you have double the number of matches.

Also, when I find code with comments that add labels like "end of xxx", I automatically delete all of these. It doesn't help me at all, and only makes searches in the code more difficult. Even the bad editors like VSCode probably have the functionality to jump to matching delimiter, which would easily reveal the name of the block you are working with.

And your company guidelines... oh, it should be fun when someone renames a namespace, but forgets to update the comments. At least, in Ada it's guaranteed that the end and the beginning will match. Also, sometimes I prefer not to invoke any kind of automatic refactoring, but rather rename a function and see what other code breaks, to quickly find dependencies. It's really annoying that this renaming must happen twice.

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

#107

Post by samatman »

lenkite wrote: post #72
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…

I never even knew that this "Ancient Language" had dependent types. Always thought it was a "modern" invention of snazzy newer academic languages like Idris, etc. But, its easy to figure out why it didn't become popular. C/C++/any other top10 language all had free compilers available to everyone. Ada didn't during the explosive era of computing expansion. Also, not a problem nowadays with IDE auto-complete/snippets b…

Verbosity was genuinely expensive at the time. Two ways: until the mid-80s, 5 1/4" floppies held between 100 and 250kB depending on format, so a program which used up three times as many bytes (I think that's a good multiplier from C to Ada) is making a meaningful difference for transfer, backups, storage.

What's probably more important is that 80 columns was far and away the likely maximum for a screen, and 40 columns wasn't unheard of. The word PROCEDURE took up 11 to 22% of the column width! This wasn't a show-stopper, Pascal uses a similar syntax (both of them derived from Algol of course) and was pretty popular, but plenty of people complained about Pascal's verbosity as well, and Ada is definitely more verbose than even Pascal.

The lack of autocomplete (even things like snippets were relatively uncommon) didn't help, but mainly, verbosity imposed real costs which are mitigated or irrelevant now.

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

#108

Post by rad_gruchalski »

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…

I really wanted to use Ada, at least learn it. Concepts are nice but I gave up when started looking into unicode support. It was wild, a bit discouraging. Or has the situation changed? What’s the unicode status in Ada?

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

#109

Post by quietbritishjim »

pjmlp wrote: post #79
mirashii wrote: post #57

Earlier quoted context omitted.

> out in the open This part was an important part of the sentence you might've missed.

https://www.gnu.org/software/gnat/

The original point is that there is only one open implementation. This is a link to that one open implementation. You are pushing this conversation around in circles.

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

#110

Post by toolslive »

alexvitkov wrote: post #75
fpoling wrote: post #65

Earlier quoted context omitted.

Explicit language support is very nice as the compiler can and do a lot of optimizations and free the space as early as possible on all control paths and ensure full memory safety. For example, when a function returns a thing on the second stack the compiler can arrange that, before returning, the thing is moved to the second stack position that was at the start of the function. This releases the memory that was used…

Doing frees/moves/copies on the second stack makes it harder to track the lifetime of allocations, and restricts what you can use it for - to free a block on the stack you necessarily have to free everything after it. Most programs have a point where you know nothing on it is used and it's convenient (and very performant) to free the entire thing, and that makes it way easier to reason about - when you alloc from it…

The point is indeed what you need to look for but why does it need to be a stack ? I guess it's just a naming thing. I've always looked at it as a scratchpad (that was heap allocated)
Post reply on HN