OneWingedShark

I think there are certain core-functionalities that could benefit from being written in SPARK -- things like the core of the OS, common networking facilities/network stack (the IRONSIDES DNS is a good step in that direction).

> Not much of a stretch with C, really - there's a reason its used to write operating systems

C is a terrible language for Operating Systems.

No modules, weak-typing, and full of gotchas and pitfalls — plus, it's answers like this that ignore the history of OSes: the Burroughs was written in Algol, Multics was written in PL/I, and VMS in BLISS (plus other languages, thanks to the design/architecture of the CLE).

> Can any of other language do that? Ada can. The biggest Ada vendor actively pushes Ada-as-an-embedded-language, which is nice in some ways, but in others it can make it seem like Ada is only for embedded.

If it were up to me to design curricula for CS, I'd do the entire thing in Ada, with the exceptions of "Data-Structures & Algorithms" being in Lisp and "Machine Architecture" in Forth — both of these classes would have a "Compilers & Interpreters" prerequisite where they would be provided the specification-files for Forth and Lisp interpreters/compilers which the students would implement, and that is what they would use in the aforementioned classes — not only would having the curriculum in these less-popular languages help emphasize that the important part is the underlying-theory (rather than hyped-up language-of-the-month), but making its prerequisites actually matter and introducing an element of software-maintenance would do a lot to produce good graduates.

> Build a toolset that yells at you when you want to do something stupid/dangerous.

Why do you think I'm a fan of Ada? (And looking to get into VHDL, too.)

Go.

Still Go.

Interesting.

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

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

>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 );

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.

> 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.)

> What has stopped people from creating a standard with no undefined behavior?

It's a lot of work.

> Is such a thing impossible? Have people done it?

It's possible; Ada has a really good take -- in that standard, there's a class of errors called "bounded errors" which on the surface look like "undefined behavior", but are a lot different in that they list out the possible results and thus preclude the "nose demons" problem of C -- see: http://www.ada-auth.org/standards/2xaarm/html/AA-1-1-5.html

If you have GCC or G++, simply use the `-fdump-ada-spec` command-line option; done.

(see: https://www.adacore.com/gems/gem-59 )

Well, there's a bit of a problem in how you're qualifying things. For example, certain things that aren't obviously handled by the type-system might be.

One example would be loops and off-by-one errors. For the case of For-loops on arrays Ada's solution arguably does so via the type-system; in Ada arrays "know" their own length, start- and stop-index and these are query-able via attributes.

So, given Function Sum( Input : Integer_Array ) return Long_Long_Integer you could for-loop on the parameter, querying the 'Range attribute -- yielding a possible implementation of:

Function Sum( Input : Integer_Array ) return Long_Long_Integer is Begin Return Result : Long_Long_Integer := 0 do For Index in Input'Range loop Sum:= Sum + Long_Long_Integer( Input(Index) ); End Loop; end return; End Sum;

And the entire problem is avoided via the type-system.

http://learnadanow.com is done by the same guy that does GetAdaNow.com

The Ada Information Clearinghouse has a section for learning Ada: http://www.adaic.org/learn/

There's a toy LISP I did as/for a tutorial, though this is the final product: https://github.com/OneWingedShark/Ada_Tutorial

And here's the home of the ARG, Ada's design group: http://ada-auth.org/