Dependently typed programming languages such as Coq and Idris let you write proofs about your programs. These languages are fairly academic, and most engineers probably won't find it worthwhile to use these tools. Personally, I love them. I wrote a short article about my experience with Coq: https://www.stephanboyer.com/post/134/my-unusual-hobby
> Do you have an example of a language that does what you're looking for?
You mean, like SPARK?
> On the proof side, Rust's built in unit testing is great, and allows for quick validation of code (proofs).
No, unit testing is not proof of correctness, it's a hint that your code has no regressions at best. I'd take a proof over unit tests any time of day.
Note that unit tests prove only that the code works for those inputs and those code paths tested. Mathematical proofs are supposed to be exhaustive.
I haven't had the time to learn it yet, though I would like to.
At least equally importantly, we need a new generation of developers to grow up with these tools before they can become the norm.
In fact, the biggest contribution that academia could make to safe programs is to replace Java and C by Rust in all the programming courses, so that the next generation of developers is raised on Rust and makes that language (and its strictness mindset) popular in the industry in the same way that Java's relevance in the industry is based (in part) on its prevalence in curriculums.
Rust isn't the first language to emphasise correctness. We've had Ada for decades, but it's not taken over the world.
Going to the extreme, full-bore formal methods will never be taught as introductory material on programming courses for the masses, but they will continue to be taught at good universities.
I'm not sure this is a bad thing. For most applications, ad-hoc develop-and-test makes good sense. RAD is important in some domains. Both formal methods and highly strict languages have their downsides.
There's more to correctness than language, of course. A shift toward correctness could be as simple as encouraging students to put runtime asserts in their Java code.
Unit testing can only proof one instance of the input domain, e.g. the function square() returns 4 under the input 2. Languages like Coq allow you to proof that the function square returns the squared input for every possible input.
I see way more future in one's ability to write proofs of correctness in the comments before the function definition in any language; rather than preferring any specific language for the sake of proof.
Do you have an example of a language that does what you're looking for?
On the proof side, Rust's built in unit testing is great, and allows for quick validation of code (proofs). But I think you mean something different.
> Go works wonderfully
Go does work wonderfully, you should definitely use what you like. For me personally, though, Go never excited me. Rust on the other hand continues to be exciting, I always feel like I'm learning something new (and I've been using it for the past 3 years).
> For example, you could always just clone memory at every occasion, return the input instead of borrowing, etc. In fact, these things might be easier for a beginner to do.
I think most Rust beginners (I know it was true of me anyway) do often just clone everywhere. Eventually, you then replace that with Rc or Arc... And then one day you decide you want the fastest thing on the block, and now you know the in's and out's of Rust, so you decide to up the ante and put lifetimes on everything.
I recommend this pattern to all Rust beginners.