4 ms·

> I would normally define 'correctness' to include rigorous mathematical proofs. Do you have an example of a language that does what you're looking for? On th

> I would normally define 'correctness' to include rigorous mathematical proofs. 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.

GolDDranks 9y ago
I think they mean something like what proof assistants like Cog and Irdis do. ATS is another language that enables proofs, and it's more geared to the systems programming use case, as it's similar to C. 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.
- jwhite 9y ago
  Sorry this comment is so late; ATS is also interesting because it has linear types that allow compile-time resource tracking similar to Rust's ownership and lifetime tracking. If you use linear types you can opt out of the garbage collector. That makes it very attractive for systems programming, and in particular embedded systems. I believe there is a demo of ATS running on an Arduino of some sort. I haven't had the time to learn it yet, though I would like to.
curryhoward 9y ago
> Do you have an example of a language that does what you're looking for? 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 https://www.stephanboyer.com/post/134/my-unusual-hobby
- lmm 9y ago
  Rust has the same level of rigour, other than lacking totality. Not having dependent types makes properties a lot more cumbersome and less practical to encode, but the actual proofs you get of the properties you do model are just as valid as those in Coq and Idris (modulo nontermination).
Zalastax 9y ago
You'd have to look at niche languages like Coq, Idris, or Agda if you want mathematical proofs. There's a lot of research that needs to be done before proven programs can become the norm.
- majewsky 9y ago
  > There's a lot of research that needs to be done before proven programs can become the norm. 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.
  - MaxBarraclough 9y ago
    As Zalastax was saying, by the standards of Coq, Rust doesn't have a strict mindset. 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.
    - Zalastax 9y ago
      I hope we'll see more advanced type features added to languages. I find it very annoying when I can't be expressive enough and have to resort to comments and runtime errors. It's a very fine line to walk though. TypeScript is the language that I think is best at walking that line currently.
Joool 9y ago
> 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. 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.
- heavenlyblue 9y ago
  And for anything more or less complex and optimised (e.g. Egalitarian Paxos), you'll not only end up with proving the correctness of the algorithm, but also the correctness of the implementation (which by themselves will hugely vary). 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.
dozzie 9y ago
>> I would normally define 'correctness' to include rigorous mathematical proofs. > 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.
Too 9y ago
C# Code Contracts can specify constraints (like range check, nullability, list sizes, etc) on inputs/outputs of functions and enforces these statically based on the code inside the function.

GolDDranks 9y ago

I think they mean something like what proof assistants like Cog and Irdis do. ATS is another language that enables proofs, and it's more geared to the systems programming use case, as it's similar to C. 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.

jwhite 9y ago
Sorry this comment is so late; ATS is also interesting because it has linear types that allow compile-time resource tracking similar to Rust's ownership and lifetime tracking. If you use linear types you can opt out of the garbage collector. That makes it very attractive for systems programming, and in particular embedded systems. I believe there is a demo of ATS running on an Arduino of some sort. I haven't had the time to learn it yet, though I would like to.

curryhoward 9y ago

> Do you have an example of a language that does what you're looking for? 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 https://www.stephanboyer.com/post/134/my-unusual-hobby

lmm 9y ago
Rust has the same level of rigour, other than lacking totality. Not having dependent types makes properties a lot more cumbersome and less practical to encode, but the actual proofs you get of the properties you do model are just as valid as those in Coq and Idris (modulo nontermination).

Zalastax 9y ago

You'd have to look at niche languages like Coq, Idris, or Agda if you want mathematical proofs. There's a lot of research that needs to be done before proven programs can become the norm.

majewsky 9y ago
> There's a lot of research that needs to be done before proven programs can become the norm. 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.
- MaxBarraclough 9y ago
  As Zalastax was saying, by the standards of Coq, Rust doesn't have a strict mindset. 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.
  - Zalastax 9y ago
    I hope we'll see more advanced type features added to languages. I find it very annoying when I can't be expressive enough and have to resort to comments and runtime errors. It's a very fine line to walk though. TypeScript is the language that I think is best at walking that line currently.

Joool 9y ago

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

heavenlyblue 9y ago
And for anything more or less complex and optimised (e.g. Egalitarian Paxos), you'll not only end up with proving the correctness of the algorithm, but also the correctness of the implementation (which by themselves will hugely vary). 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.

dozzie 9y ago

>> I would normally define 'correctness' to include rigorous mathematical proofs. > 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.

Too 9y ago

C# Code Contracts can specify constraints (like range check, nullability, list sizes, etc) on inputs/outputs of functions and enforces these statically based on the code inside the function.