I found that learning Ada was a good way to learn how to write good C++ code, because both languages are at the same level of abstraction but Ada is clean and opinionated.
The best a example is RAII. This is a pattern in C++ that you have to follow if you don't want to make a mess. In Ada it's a language feature called Controlled Types.
I know there is a belief that Rust/Ada etc is safer than C/C++ and in some cases that is true. I know of multiple, airworthy aircraft that are flying with C++ code. I also know of aircraft flying with Ada. The aircraft flying with Ada is hard to maintain. There is also a mountain of testing that goes into it that is not just unit testing. This mountain of integration, subsystem and system level testing is required regardless
They have different definitions of failure. In Lean a failure is to calculate wrong thing. In SPARK a failure is to not calculate at all because of memory issue or something like this. As far as I've seen SPARK, it encourages ephemeral data structures and effectful computations. Lean is less familiar to me, but I've got the impression that it is about correct computation in infinite memory and stack, and value-centered computations are encouraged. SPARK did not have pointers for long period. Then SPARK has got pointers, but only unique ones. Lean has shared pointers to immutable data structures. And infinitely recursive data structures.
Yet another provable code I have found in Eiffel. There is "proven" doubly linked list in Eiffel. Something not possible in SPARK, going against unique pointers. Something not possible in Lean, going against immutability.
I'm not sure I'd want to limit the selection of languages that much. Depending on the project and how much language risk you can manage (as opposed to security risk), there also is D, Odin, and Zig. And probably a bunch more I'm unfamiliar with.
Alternatively, just get better at C/C++… It isn’t going anywhere, and it feels like more developers are coming around to the idea that maybe security guarantees are not worth throwing the baby out with the bath water.
Can we please stop with the "git gud" excuse? When even expert teams with decades of experience keep making mistakes, we need to recognize that C/C++ are fundamentally flawed and should be replaced with something better.
Personally I think Swift can be a good choice that is more familiar to existing C++ developers than the others, and a lot of people seem to be sleeping on it.
It has full native interop with C and C++ so you can already use all your existing libraries. Historically it lacked cross-platform support but this is not true anymore. It does lack a native GUI framework, but for now you can keep using C++ ones.
Some people complain about its ties to Apple, but hopefully with it gaining much wider cross-platform support, it may not matter that much in the future, but I guess it remains to be seen.
Their example of why Ada has better strong typing than Rust is that you can have floats for miles and floats for kilometers and not get them mixed up. News flash, Rust has newtype structs, and you can also do basically the same thing in C++.
I don't know much about Ada. Is its type system any better than Rust's?
> If you’re prepared to look at alternative programming languages to avoid the costs and risks of C/C++, SPARK offers an opportunity to go much further than Ada or Rust. SPARK, which is based on Ada, offers industrial-strength formal methods: an opportunity for you to prove mathematically that your software is safe and secure. This paradigm shift in software development methodology offers significant cost savings for high-integrity software.
Forgive me if I sound naive but I always found it a bit weird how something like this is touted as a strength of Ada, but never actually demonstrated in comparison with a heavily typed language like Rust. Regardless of the language, you cannot write some special program that guarantees an input will be valid if it comes from an external source or a human. It is simply impossible to prove this at compile time. What you can do in rust, and other languages, is check you're within boundaries and throw an exception if it's out of bounds.
Herein lies the issue: "You can't throw exceptions in this kind of software". True. So how do you prove it WONT go out of bounds at compile time, if the input isn't trusted? Rustacians get picked on a lot for spending more time on type-theory than actually writing working code, but from my perspective it looks worse in Ada, obsessing over proving something in a complete vacuum that can't possibly account for all possible invariants in the real world.
How does Ada/Spark compare to theorem provers like Agda and Lean, in terms of guarantees?
I’m not really into languages like this. Anybody got some resources regarding how strict the guarantees can get in either of these types of environments?
The average HN comment section has kind of become a new reddit and I'm kind of pessimistic about it. I see the same low effort comments lately, and I moved away from Reddit for that very reason. Maybe these type of questions just attract the same people.
I might be in the minority, but I hate type re-definitions, I want types to just tell me how much memory a variable is using and it’s bit interpretation. Every variable already has a name, use that to communicate the data’s representation and if it’s really important that representation mismatches are caught at compile time wrap it in a struct. I don’t want to guess how much memory the compiler decided a variable needed (though that is also present to an extent in C/C++)
28 comments
[ 3.8 ms ] story [ 47.1 ms ] threadThe best a example is RAII. This is a pattern in C++ that you have to follow if you don't want to make a mess. In Ada it's a language feature called Controlled Types.
Yet another provable code I have found in Eiffel. There is "proven" doubly linked list in Eiffel. Something not possible in SPARK, going against unique pointers. Something not possible in Lean, going against immutability.
It has full native interop with C and C++ so you can already use all your existing libraries. Historically it lacked cross-platform support but this is not true anymore. It does lack a native GUI framework, but for now you can keep using C++ ones.
Some people complain about its ties to Apple, but hopefully with it gaining much wider cross-platform support, it may not matter that much in the future, but I guess it remains to be seen.
I don't know much about Ada. Is its type system any better than Rust's?
https://www.adacore.com/nvidia
Forgive me if I sound naive but I always found it a bit weird how something like this is touted as a strength of Ada, but never actually demonstrated in comparison with a heavily typed language like Rust. Regardless of the language, you cannot write some special program that guarantees an input will be valid if it comes from an external source or a human. It is simply impossible to prove this at compile time. What you can do in rust, and other languages, is check you're within boundaries and throw an exception if it's out of bounds.
Herein lies the issue: "You can't throw exceptions in this kind of software". True. So how do you prove it WONT go out of bounds at compile time, if the input isn't trusted? Rustacians get picked on a lot for spending more time on type-theory than actually writing working code, but from my perspective it looks worse in Ada, obsessing over proving something in a complete vacuum that can't possibly account for all possible invariants in the real world.
I’m not really into languages like this. Anybody got some resources regarding how strict the guarantees can get in either of these types of environments?
1) On Formal Methods Thinking in Computer Science Education - https://dl.acm.org/doi/10.1145/3670419
2) (In-)Formal Methods: The Lost Art --- A Users’ Manual by Carroll Morgan - https://fme-teaching.github.io/2019/10/03/in-formal-methods-...
3) Forthcoming book by Carroll Morgan Formal Methods, Informally How to Write Programs That Work - https://www.cambridge.org/highereducation/books/formal-metho...
4) Understanding Formal Methods by Jean-Francois Monin - A firehose of information.
I really like the other compilers he worked on, e.g., SPITBOL, SETL
He taught CS but he studied chemistry as a student