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

121–130 of 146 posts

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

#121

Post by kevlar700 »

LiamPowell wrote: post #7
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'm a bit disappointed that we've ended up with Rust in the kernel but not Ada. The kernel relies on GCC and there's already an Ada compiler in GCC, so it wouldn't require adding another compiler as a build requirement like Rust does. There's a couple of major advantages that Ada could have in the Linux over Rust for safe drivers: 1. Having the option to use SPARK for fully verified code provides a superset of the co…

Agreed. It would also alleviate the maintenance issue as Ada was designed to reduce software costs. Realistically the obly way this will have any chance is if a few developers were funded full time to work on it. There seemed to be a few full time devs pushing Rust support and some drivers before it was taken seriously. Honestly Ada is the best language that I have seen for drivers and for network stacks or for registers received as bytes. Linux is missing out.

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

#122

Post by kevlar700 »

jjnoakes wrote: post #69
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…

Memory safety and the borrow checker are useful even in the absence of dynamic memory allocation. This still doesn't bring rust and ada to the same place, but it is important to clarify that piece.

Spark supports borrowing which is easier to use than Rusts now. It also prevents memory leaks.

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

#123

Post by Yoric »

kevlar700 wrote: post #120
Yoric wrote: post #104

Earlier quoted context omitted.

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.

The real benefit of Adas typing is that it is so easy to utilise often preventing logic errors.

And this is definitely a strong benefit.

The benefit of Rust's typing is that (in the absence of `unsafe` or bugs in the compiler or stdlib), it's a simple theorem prover. Much less powerful than the theorem provers you can use with SPARK, but it's a start :)

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

#126

Post by ksec »

LiamPowell wrote: post #7
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'm a bit disappointed that we've ended up with Rust in the kernel but not Ada. The kernel relies on GCC and there's already an Ada compiler in GCC, so it wouldn't require adding another compiler as a build requirement like Rust does. There's a couple of major advantages that Ada could have in the Linux over Rust for safe drivers: 1. Having the option to use SPARK for fully verified code provides a superset of the co…

>ended up with Rust in the kernel but not Ada

Linus hated Ada. I suspect he doesn't exactly like Rust either but the Tribe is just too strong within Linux.

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

#127

Post by Lucretia9 »

bobajeff wrote: post #87
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…

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.

What are the options required to build an android gcc these days?

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

#128

Post by Lucretia9 »

LtWorf wrote: post #17
LiamPowell wrote: post #7

Earlier quoted context omitted.

I'm a bit disappointed that we've ended up with Rust in the kernel but not Ada. The kernel relies on GCC and there's already an Ada compiler in GCC, so it wouldn't require adding another compiler as a build requirement like Rust does. There's a couple of major advantages that Ada could have in the Linux over Rust for safe drivers: 1. Having the option to use SPARK for fully verified code provides a superset of the co…

rust is in the kernel to attract the young developers, which ada does not.

GetIntoGamedev is not old, he's in his 20's. The issue is, is that people are not prepared to trying something if it doesn't look like C or C++.

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

#129

Post by Lucretia9 »

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…

You talk about C and C++ yet call Ada "ancient," C from 1969 and C++ from 1979.

Whereas Ada's first version is from 1980 and first standardised version (different to 1980) in 1983. Yeah, "ancient."

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

#130

Post by Lucretia9 »

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.

Pretty sure Java in vscode and android studio places block names after }'s because it's hard to read otherwise.
Post reply on HN