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

Why Ada Is the Language You Want to Be Programming Your Systems With

hackaday.com

Post reply on HN
Print view View original

321–330 of 330 posts

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#321

Post by OneWingedShark »

ajxs wrote: post #191

I live near Sydney University ( not my alma-mater ). In a rather serendipitous turn, one day on my way home from the shops I was walking past one of the USYD buildings and there was a giant stack of library books that had thrown out onto the sidewalk as rubbish to be collected by the council. It turns out they were old science faculty books that were no longer prescribed material. I started looking through them and f…

> if this post had been three days later I'd have been able to link the finished product here right now.

Well, that was 5 days ago, which means you CAN post the link! (I'd like to see it, quite a lot.)

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#322

Post by OneWingedShark »

Ono-Sendai wrote: post #249
antocv wrote: post #243

Earlier quoted context omitted.

I still cannot forgive Rust for not learning anything from Ada. "Code is read more often than it is written". Reading Ada is so unambigous, and clear. If you mean if then, you have the keyword then, when you want to say procedure you say procedure and you can read that. Rust? fn, because is it fun, or functor, so fuck you.

Do you really want to type out 'procedure' thousands of times?

Yes. Because the alternative is idiotic, hard to read BS like fn.

The problem is that "fn" is optimizing the WRONG things: not only is your code going to be read more than it is ever written, but this abbreviated form is actively hostile towards domain-level subject-matter experts that you may want to audit or verify your code. Now, instead of him jumping into code that reads like English (Ada), now he has to 'decode' Rust BEFORE AND DURING his evaluation of the code, distracting him from his purpose.

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#323

Post by OneWingedShark »

steveklabnik wrote: post #292
johnisgood wrote: post #288

Earlier quoted context omitted.

And this is worth noting: > These runtime checks[1] are costly, both in terms of program size and execution time. It may be appropriate to remove them if we can statically ensure they aren't needed at runtime, in other words if we can prove that the condition tested for can never occur. > This is where the analysis done by GNATprove comes in. It can be used to demonstrate statically that none of these errors can ever…

The rust compiler also removes bounds checks and such if it can statically prove that they won't occur. You don't have as much tooling to communicate it to the compiler as you do in SPARK just yet. When I learned Ada (blog post somewhere in this thread) I was pretty shocked by how many more runtime checks it had than Rust does, overall. Rust usually checks things at compile time.

>When I learned Ada (blog post somewhere in this thread) I was pretty shocked by how many more runtime checks it had than Rust does, overall. Rust usually checks things at compile time.

That's perhaps an oversimplification; elsewhere it's been said of Ada's mentality that "Incorrect Is Simply Not Allowed." — but there's ALWAYS been a preference for pushing checks from dynamic to static, and from runtime to compile-time.

As a trivial example, the following code is typically generated without any sort of index check because the loop-control variable takes its range from the Array, it's obvious that it CANNOT be an invalid index, and this is allowed by the language reference manual (and encouraged by the annotated reference manual)—

    For Index in Input'Range loop
        Input(Index):= 0; -- Zero the array.
    End loop;
Conversely, there are places where you cannot statically determine the validity:

    Value : Positive := Positive'Value( Get_Line );

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#324

Post by OneWingedShark »

roca wrote: post #218
ajxs wrote: post #195

Earlier quoted context omitted.

Ada is miles ahead of Rust when it comes to C interoperability. I posted this before in one of the other Rust threads, but you can't get more than two paragraphs through the official Rust FFI documentation ( https://doc.rust-lang.org/nomicon/ffi.html ) before being asked to install a third-party dependency. The 'Interfaces.C' package is defined in the Ada language specification. And, as others have mentioned, Ada's l…

There's nothing wrong with pulling in the `libc` dependency. It literally means adding two lines of code and then `cargo` manages everything for you. It isn't really third-party; the owner is "rust-lang:libs". I understand that people are conditioned to think APIs are easier to consume when they're in the standard library, because that's true in many languages, especially those that lack a modern package management s…

> There's nothing wrong with pulling in the `libc` dependency.

Yes, there is. Not only is dependency transitive: you now depend on everything libc depends on — but now you're depending on the correctness AND properties of the dependency, to include security.

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#325

Post by OneWingedShark »

topspin wrote: post #120
ebaustin wrote: post #13

Earlier quoted context omitted.

Also if you've written any PL/SQL stored procedures in Oracle.

PL/SQL has remained faithful to the Ada zeitgeist. I've found spotting flaws in PL/SQL during peer review to be easier than some other languages.

Interesting.

I wonder how nice a PL/SQL & Ada combined environment/IDE could be.

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#326

Post by OneWingedShark »

lone_haxx0r wrote: post #194
johnisgood wrote: post #139

Earlier quoted context omitted.

Might as well mention F* then! > F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C, WASM, or ASM code. This enables verifying…

And the "worst name" prize goes to ...

Go.

Still Go.

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#327

Post by ajxs »

OneWingedShark wrote: post #321
ajxs wrote: post #191

I live near Sydney University ( not my alma-mater ). In a rather serendipitous turn, one day on my way home from the shops I was walking past one of the USYD buildings and there was a giant stack of library books that had thrown out onto the sidewalk as rubbish to be collected by the council. It turns out they were old science faculty books that were no longer prescribed material. I started looking through them and f…

> if this post had been three days later I'd have been able to link the finished product here right now. Well, that was 5 days ago, which means you CAN post the link! (I'd like to see it, quite a lot.)

Don't worry, I haven't forgotten about these comments. It's taking me a little longer than expected due to a few other commitments. I'm just in the process of cleaning the code up and doing the documentation, so I'll have this up very soon.

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#328

Post by johnisgood »

OneWingedShark wrote: post #323
steveklabnik wrote: post #292

Earlier quoted context omitted.

The rust compiler also removes bounds checks and such if it can statically prove that they won't occur. You don't have as much tooling to communicate it to the compiler as you do in SPARK just yet. When I learned Ada (blog post somewhere in this thread) I was pretty shocked by how many more runtime checks it had than Rust does, overall. Rust usually checks things at compile time.

>When I learned Ada (blog post somewhere in this thread) I was pretty shocked by how many more runtime checks it had than Rust does, overall. Rust usually checks things at compile time. That's perhaps an oversimplification; elsewhere it's been said of Ada's mentality that "Incorrect Is Simply Not Allowed." — but there's ALWAYS been a preference for pushing checks from dynamic to static, and from runtime to compile-ti…

More information about Get_Line: https://blog.adacore.com/formal-verification-of-legacy-code

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#329

Post by ajxs »

OneWingedShark wrote: post #321
ajxs wrote: post #191

I live near Sydney University ( not my alma-mater ). In a rather serendipitous turn, one day on my way home from the shops I was walking past one of the USYD buildings and there was a giant stack of library books that had thrown out onto the sidewalk as rubbish to be collected by the council. It turns out they were old science faculty books that were no longer prescribed material. I started looking through them and f…

> if this post had been three days later I'd have been able to link the finished product here right now. Well, that was 5 days ago, which means you CAN post the link! (I'd like to see it, quite a lot.)

Here's my initial implementation: https://github.com/ajxs/cxos I'm going to continue to work on it for some time, but this is the minimal working example that I had enough time to properly document.

Re: Why Ada Is the Language You Want to Be Programming Your Systems With

#330

Post by ajxs »

crucini wrote: post #203
ajxs wrote: post #191

I live near Sydney University ( not my alma-mater ). In a rather serendipitous turn, one day on my way home from the shops I was walking past one of the USYD buildings and there was a giant stack of library books that had thrown out onto the sidewalk as rubbish to be collected by the council. It turns out they were old science faculty books that were no longer prescribed material. I started looking through them and f…

I look forward to seeing your OS example.

As I posted in another comment, here's my initial implementation: https://github.com/ajxs/cxos Apologies for the double post. I just wanted to ensure that you would see the reply.
Post reply on HN