RamaSpaceShip wrote: ↑Fri Jun 05, 2020 10:16 pm
Having written a few hundred thousand lines in Java and C#, for me, there is a big difference between the two languages, even if they seem similar.
Java and C# are certainly in the same class of languages even if their details a very different. That class being: languages designed to compile down to some kind of bytcode, require an interpreter to run them, hopefully cross platform executables, object oriented, with a syntax that looks a lot like C/C++, some kind of memory safety through the use of garbage collection..
My statement about the benefits of learning a language very different from Java/C# was about getting out of that class. Learning a language in a different class that does things differently. Gives one a different perspective on what programming is. Haskell for example for that functional programming view. C/C++ to get an idea about what a stack and heap actually is. Heck even an assembly language so you get some idea how computers work.
I notice on clicking on the first example their, pi digits, that the C# code use the GMP multiple precision library. Which is written in C. That benchmark is comparing C to C++ mostly!
RamaSpaceShip wrote: ↑Fri Jun 05, 2020 10:16 pm
On a big project, this appears as a very little impact as you can still implement a specific algorithm in the most efficient language for it, and use native calls..
I'm sure that is true. When your high level language is just glue code for using tones of libraries and run time code written in C/C++ then the fact that C# is so slow matters less. See above.
RamaSpaceShip wrote: ↑Fri Jun 05, 2020 10:16 pm
I see your point for the safety of memory: formally proven.
You need a subset of Ada for that (for what Spark is meant) , but for Rust as well : 'unsafe' must be removed, as it can break everything.
In addition, there is no formal definition of Rust. So it is difficult to formally prove it as a whole.
Rust is pretty new, it has undergone a lot of changes since ten years ago. Only reaching stability and version 1 a couple of years back. So yes, a formal definition is missing. It's being worked on:
https://rust-lang-nursery.github.io/wg-verification/ There are a lot of people in the safety critical and secure software worlds asking for that.
RamaSpaceShip wrote: ↑Fri Jun 05, 2020 10:16 pm
If you hide pointers in specially crafted classes in Ada (you can even tell the Ada compiler to prohibit the use of allocators in the part of the code you want), you get the same safety as Rust which hides 'unsafe' in its libraries.
That's not formally provable, but it seems to me very similar!
I think the point is that the safe subset of Ada, Spark, has limitations that annoy users and they have been asking for those limitations to be removed. As he article I linked to above says the Spark guys realized how to remove those limitations when they saw how Rust does it.
Memory in C++ is a leaky abstraction .