www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - D enters Tiobe top 20

reply RazvanN <razvan.nitu1305 gmail.com> writes:
Good news, everyone!

D has entered the Tiobe top 20 ranking of programming languages 
[1], landing on the 18th position. I have been keeping an eye on 
this index, and it is for the first time that I see this 
happening.

Cheers,
RazvanN

[1] https://www.tiobe.com/tiobe-index/
Nov 04
next sibling parent reply Daniel Kozak <kozzi11 gmail.com> writes:
On Mon, Nov 4, 2019 at 10:05 AM RazvanN via Digitalmars-d
<digitalmars-d puremagic.com> wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming languages
 [1], landing on the 18th position. I have been keeping an eye on
 this index, and it is for the first time that I see this
 happening.

 Cheers,
 RazvanN

 [1] https://www.tiobe.com/tiobe-index/
AFAIK, it has been there before, but for very short time: https://forum.dlang.org/post/fdmafvxoawgmsfjmhksr forum.dlang.org
Nov 04
next sibling parent RazvanN <razvan.nitu1305 gmail.com> writes:
On Monday, 4 November 2019 at 09:19:16 UTC, Daniel Kozak wrote:
 On Mon, Nov 4, 2019 at 10:05 AM RazvanN via Digitalmars-d 
 <digitalmars-d puremagic.com> wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming 
 languages [1], landing on the 18th position. I have been 
 keeping an eye on this index, and it is for the first time 
 that I see this happening.

 Cheers,
 RazvanN

 [1] https://www.tiobe.com/tiobe-index/
AFAIK, it has been there before, but for very short time: https://forum.dlang.org/post/fdmafvxoawgmsfjmhksr forum.dlang.org
I started looking into D in October 2016, so I did not know about that (the post is from June 2016). Anyway, I think the community should take pride in this outcome and we should do our best to make sure D stays in the top 20. Best regards, RazvanN
Nov 04
prev sibling parent reply IGotD- <nise nise.com> writes:
On Monday, 4 November 2019 at 09:19:16 UTC, Daniel Kozak wrote:
 On Mon, Nov 4, 2019 at 10:05 AM RazvanN via Digitalmars-d 
 <digitalmars-d puremagic.com> wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming 
 languages [1], landing on the 18th position. I have been 
 keeping an eye on this index, and it is for the first time 
 that I see this happening.

 Cheers,
 RazvanN

 [1] https://www.tiobe.com/tiobe-index/
AFAIK, it has been there before, but for very short time: https://forum.dlang.org/post/fdmafvxoawgmsfjmhksr forum.dlang.org
I think D is going to stay in the top segment now, because of C++xx. Many people are seeking a new programming language and D is one refuge. Also that it got into the GNU compiler collection also helps. D can copy the success of Python, being expressive and simple. Hopefully, the D community keep D simple and do not add a lot of crud like in C++xx. Aesthetic design in programming languages matters, just as they do with cars. Speaking of Rust, I think Rust will remain a niche language because it is a bit too complicated than what benefits it gives. A programmer who only used Python before is going to choose D over Rust and that's where the masses are. Keep up the good work.
Nov 04
next sibling parent reply Paolo Invernizzi <paolo.invernizzi gmail.com> writes:
On Monday, 4 November 2019 at 10:56:29 UTC, IGotD- wrote:
 On Monday, 4 November 2019 at 09:19:16 UTC, Daniel Kozak wrote:
 A programmer who only used Python before is going to choose D 
 over Rust and that's where the masses are.
I think you are really right, especially with a good framework for example for machine learning. Alas with a good deep learning D solution, we will for sure use D for that, instead of doing the work in python, and then translating the successful one into C++ for performance and embedding, for example.
Nov 06
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Wednesday, 6 November 2019 at 09:18:58 UTC, Paolo Invernizzi 
wrote:
 Alas with a good deep learning D solution, we will for sure use 
 D for that, instead of doing the work in python, and then 
 translating the successful one into C++ for performance and 
 embedding, for example.
Out of curiosity, does that mean that you prefer to do the training on your own machines rather than "renting" existing infrastructure (cloud solutions)? Having little experience with deep learning (although some with basic ML), I thought the advantage of using a ready-made like the Python one from Google is that you have a large set of prewritten libraries from both Google and other third party contributors that you can compose? Also, if you create your own training-environment, you would still have to run it on a cluster with GPUs? Then distill it down into something that can run well on a single CPU/GPU/SoC? Maybe a framework can do that translation well... but I guess then the better option would be to have a dedicated high level language that translates well to both the training-environment and the final host environment. That seems more reasonable to me? Or maybe you talk about the initial preprocessing of data? In which case you can do it now by interfacing with Python from D?
Nov 06
prev sibling parent reply bachmeier <no spam.net> writes:
On Monday, 4 November 2019 at 10:56:29 UTC, IGotD- wrote:

 Speaking of Rust, I think Rust will remain a niche language 
 because it is a bit too complicated than what benefits it 
 gives. A programmer who only used Python before is going to 
 choose D over Rust and that's where the masses are.
I'm not going to speculate about Rust's future, but that's consistent with my story. I used Rust before using D. Rust had all the hype and D was selling itself as a dialect of C++ in those days, so the decision to go with Rust was easy. It didn't take long to realize that Rust was not going to work. It has a learning curve like Vim. That meant that even ignoring the hideous syntax, which might be better now, nobody I was working with (the Python type of programmer) was ever going to write a line of Rust. It was hard to understand what it brought to the table for most of the programming world. After trying Go and not liking that either, I decided to give D a try during a free moment one evening, expecting to not spend more than a few minutes on it. What I found was a surprisingly well-designed language that had little in common with C++ other than the common ancestor of C. For anyone looking at compiled languages for speed, D was miles ahead of anything else in terms of the combination of ease of use and features.
Nov 06
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/6/2019 2:31 AM, bachmeier wrote:
 That meant that even ignoring the hideous syntax
I seriously don't like that syntax, either. The Ownership/Borrowing scheme for D does not introduce ANY new syntax other than live. It'll look just like the code you're used to!
Nov 06
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 07.11.19 01:03, Walter Bright wrote:
 On 11/6/2019 2:31 AM, bachmeier wrote:
 That meant that even ignoring the hideous syntax
I seriously don't like that syntax, either. The Ownership/Borrowing scheme for D does not introduce ANY new syntax other than live. It'll look just like the code you're used to!
That's not a plus. It will _mean_ something else. Therefore, you will have trouble at the interface between live and non- live code, because it is not the same language. Not to mention that live without any further syntax changes will necessarily be even more restrictive than safe Rust.
Nov 07
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/7/2019 1:45 AM, Timon Gehr wrote:
 That's not a plus. It will _mean_ something else. Therefore, you will have 
 trouble at the interface between  live and non- live code, because it is not
the 
 same language. Not to mention that  live without any further syntax changes
will 
 necessarily be even more restrictive than safe Rust.
I guess we'll have to see. I'm making progress every day on it. I'm looking forward to you tearing it apart :-)
Nov 08
parent Timon Gehr <timon.gehr gmx.ch> writes:
On 08.11.19 11:11, Walter Bright wrote:
 On 11/7/2019 1:45 AM, Timon Gehr wrote:
 That's not a plus. It will _mean_ something else. Therefore, you will 
 have trouble at the interface between  live and non- live code, 
 because it is not the same language. Not to mention that  live without 
 any further syntax changes will necessarily be even more restrictive 
 than safe Rust.
I guess we'll have to see. I'm making progress every day on it. I'm looking forward to you tearing it apart :-)
So am I. I'm dispersing preliminary advice primarily to make that task more challenging. I'd be delighted to fail. ;)
Nov 08
prev sibling next sibling parent Jacob Carlborg <doob me.com> writes:
On Monday, 4 November 2019 at 09:03:04 UTC, RazvanN wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming languages 
 [1], landing on the 18th position. I have been keeping an eye 
 on this index, and it is for the first time that I see this 
 happening.
I'm surprised that D is so high up in the list. There are many languages below D that I thought would be ahead, especially Go. -- /Jacob Carlborg
Nov 04
prev sibling next sibling parent reply NaN <divide by.zero> writes:
On Monday, 4 November 2019 at 09:03:04 UTC, RazvanN wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming languages 
 [1], landing on the 18th position. I have been keeping an eye 
 on this index, and it is for the first time that I see this 
 happening.

 Cheers,
 RazvanN

 [1] https://www.tiobe.com/tiobe-index/
You'd think with all the press rust seems to be getting lately it'd be higher up than it is?
Nov 04
next sibling parent reply RazvanN <razvan.nitu1305 gmail.com> writes:
On Monday, 4 November 2019 at 09:32:56 UTC, NaN wrote:
 On Monday, 4 November 2019 at 09:03:04 UTC, RazvanN wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming 
 languages [1], landing on the 18th position. I have been 
 keeping an eye on this index, and it is for the first time 
 that I see this happening.

 Cheers,
 RazvanN

 [1] https://www.tiobe.com/tiobe-index/
You'd think with all the press rust seems to be getting lately it'd be higher up than it is?
It kind of sucks that even in the announce on the Tiobe site they say "Rust is at its peak", even though it is on the 25th position, but they do not mention anything about D getting in the top 20. I think that all this Rust hype is artificial and people with large codebases that started looking into it are not that pleased with it.
Nov 04
parent reply JN <666total wp.pl> writes:
On Monday, 4 November 2019 at 09:36:33 UTC, RazvanN wrote:
 I think that all this Rust hype is artificial and people with 
 large codebases that started looking into it are not that 
 pleased with it.
It's not artificial at all. Many big companies start their projects in Rust now. Rust became the go-to language for new projects that would use C/C++ normally. They definitely have the hype behind it and the hype helps build its ecosystem, which will be helpful in maintaining the popularity after the hype dies over.
Nov 04
parent reply drug <drug2004 bk.ru> writes:
On 11/4/19 2:17 PM, JN wrote:
 On Monday, 4 November 2019 at 09:36:33 UTC, RazvanN wrote:
 I think that all this Rust hype is artificial and people with large 
 codebases that started looking into it are not that pleased with it.
It's not artificial at all. Many big companies start their projects in Rust now. Rust became the go-to language for new projects that would use C/C++ normally. They definitely have the hype behind it and the hype helps build its ecosystem, which will be helpful in maintaining the popularity after the hype dies over.
Yeah. Also some companies try to drop the current language for Rust and then after some time of Rust experience switch back. Considering huge hype about Rust and comparing it to Go it's obviously that something is wrong with Rust adopting. I totally agree to Andrei about Rust and I think it is a good but niche language and with abnormal hype.
Nov 04
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/4/2019 11:52 PM, drug wrote:
 Yeah. Also some companies try to drop the current language for Rust and then 
 after some time of Rust experience switch back. Considering huge hype about
Rust 
 and comparing it to Go it's obviously that something is wrong with Rust
adopting.
 I totally agree to Andrei about Rust and I think it is a good but niche
language 
 and with abnormal hype.
I'm going to speculate that Rust is a bit like pure functional programming. It's a great paradigm, but is inconvenient for that last mile of the code one needs to write. I've struggled with getting that last mile done with other languages (Pascal), and it would consume an inordinate amount of time. This is why D has "pure" functions. You can slip in and out of functional programming as you like. I'm working on an ownership/borrowing system for D. But the idea is it will only be active in functions marked as live.
Nov 05
next sibling parent reply drug <drug2004 bk.ru> writes:
On 11/6/19 8:02 AM, Walter Bright wrote:
 I'm going to speculate that Rust is a bit like pure functional 
 programming. It's a great paradigm, but is inconvenient for that last 
 mile of the code one needs to write. I've struggled with getting that 
 last mile done with other languages (Pascal), and it would consume an 
 inordinate amount of time.
I like your simile. Some developers complain that working with hardware in Rust means huge amount of unsafe code. The last mile in Rust can be really difficult.
 
 This is why D has "pure" functions. You can slip in and out of 
 functional programming as you like.
 
 I'm working on an ownership/borrowing system for D. But the idea is it 
 will only be active in functions marked as  live.
For example in Rust it's very hard to implement tree where nodes can point to both its parent and children because in trivial case both parent and child node are borrow each other that is impossible in Rust.
Nov 06
next sibling parent reply IGotD- <nise nise.com> writes:
On Wednesday, 6 November 2019 at 09:40:29 UTC, drug wrote:
 On 11/6/19 8:02 AM, Walter Bright wrote:

 For example in Rust it's very hard to implement tree where 
 nodes can point to both its parent and children because in 
 trivial case both parent and child node are borrow each other 
 that is impossible in Rust.
Trees are like computer science fundamentals and they are located in a wide variety of programs. Having a link to the parent is mandatory for doing a fast sorted walk through the elements in tree. You can do it rust but that means unsafe code and also you cannot use the memory management of Rust. Maybe with a reference counted object it will be easier. I'm trying to wrap my head around that they created a language that cannot support simple, common and fundamental algorithms used for more than a half of a century. The designers of Rust should have known better.
Nov 06
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Wednesday, 6 November 2019 at 11:43:30 UTC, IGotD- wrote:
 I'm trying to wrap my head around that they created a language 
 that cannot support simple, common and fundamental algorithms 
 used for more than a half of a century. The designers of Rust 
 should have known better.
Depends on what you think Rust safe-mode is. If you view it as high level language then that is OK as it can be done as an ADT. That means you have to create ADTs outside the safe language. If writing such ADTs are not possible in Rust, then that would be more of a meta-programming deficiency than a type system deficiency (or both). Reference counting and garbage collection are not alternatives, in the general case... that is way too slow... There are no safe alternatives to Rust's model, in the general case, if you want to allow arbitrary optimizations. Although you can do it in Rusts model with node-ids and indexes, but that is only efficient if you know the upper bound of the number of nodes. So, while Rust's model isn't perfect, there are no known competitive alternative models that work for graphs on the heap either! It is waaay to early to judge Rust, they have not hit the end of the road yet. We'll have to wait and see what their meta-programming ADT and type-system story evolves into.
Nov 06
prev sibling parent reply drug <drug2004 bk.ru> writes:
On 11/6/19 2:43 PM, IGotD- wrote:
 Trees are like computer science fundamentals and they are located in a 
 wide variety of programs. Having a link to the parent is mandatory for 
 doing a fast sorted walk through the elements in tree. You can do it 
 rust but that means unsafe code and also you cannot use the memory 
 management of Rust. Maybe with a reference counted object it will be 
 easier.
Yes, I wasn't clear on that. Of course I meant it is hard in safe Rust. Just because in other case there is no reason to use Rust at all I believe
 
 I'm trying to wrap my head around that they created a language that 
 cannot support simple, common and fundamental algorithms used for more 
 than a half of a century. The designers of Rust should have known better.
 
Nov 06
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Wednesday, 6 November 2019 at 12:14:33 UTC, drug wrote:
 Yes, I wasn't clear on that. Of course I meant it is hard in 
 safe Rust.
 Just because in other case there is no reason to use Rust at 
 all I believe
Well, I think Rust-developers have been overselling that aspect of Rust, but you could make the exact same argument for D. If you benchmark against standard C++ practices then Rust borrowing only replaces some common cases of RAII in C++. If you cannot do it in a RAII-fashion in C++ then you cannot do it in Rust safe mode either. You can make the exact same argument for D, though. And C++! So, all 3 languages have a safe/unsafe dichotomy that can only be resolved fully with ADTs. In C++ it is checked in code reviews and by tooling, while Rust and D codifies that informal practice in the language to some extent. In order to convince others that D is a better C++ alternative than Rust you'd have to argue encapsulation, meta-programming, composability of ADTs and available frameworks that provide ADTs. Basically do a comparison that shows that you can more easily in unsafe-mode build ADTs that competes with commonly used best-practice domain-specific C++ ADTs. And that using them in safe-mode is more convenient than in the competing languages (with comparable memory/speed performance).
Nov 06
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/6/2019 1:40 AM, drug wrote:
 On 11/6/19 8:02 AM, Walter Bright wrote:
 I'm going to speculate that Rust is a bit like pure functional programming. 
 It's a great paradigm, but is inconvenient for that last mile of the code one 
 needs to write. I've struggled with getting that last mile done with other 
 languages (Pascal), and it would consume an inordinate amount of time.
I like your simile. Some developers complain that working with hardware in Rust means huge amount of unsafe code. The last mile in Rust can be really difficult.
For comparison, the last mile in C is quite straightforward. That instantly seduced me.
 For example in Rust it's very hard to implement tree where nodes can point to 
 both its parent and children because in trivial case both parent and child
node 
 are borrow each other that is impossible in Rust.
Speaking as someone who's only Rust experience is reading the manual, there seems to be a lot of dependence on library code that is implemented in unsafe Rust. Not that this is necessarily a bad thing, as I also promote the safe/unsafe code dichotomy. D needs to make safe the default, though.
Nov 06
next sibling parent reply drug <drug2004 bk.ru> writes:
On 11/7/19 3:00 AM, Walter Bright wrote:
 Not that this is necessarily a bad thing, as I also promote the 
 safe/unsafe code dichotomy.
 
And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
 D needs to make  safe the default, though.
No doubts
Nov 06
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 07.11.19 08:34, drug wrote:
 On 11/7/19 3:00 AM, Walter Bright wrote:
 Not that this is necessarily a bad thing, as I also promote the 
 safe/unsafe code dichotomy.
And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
http://plv.mpi-sws.org/rustbelt/
Nov 07
next sibling parent drug <drug2004 bk.ru> writes:
On 11/7/19 12:41 PM, Timon Gehr wrote:
 On 07.11.19 08:34, drug wrote:
 On 11/7/19 3:00 AM, Walter Bright wrote:
 Not that this is necessarily a bad thing, as I also promote the 
 safe/unsafe code dichotomy.
And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
http://plv.mpi-sws.org/rustbelt/
I think that Rust is a good language. I'm against cargo cult.
Nov 07
prev sibling next sibling parent drug <drug2004 bk.ru> writes:
On 11/7/19 12:41 PM, Timon Gehr wrote:
 On 07.11.19 08:34, drug wrote:
 On 11/7/19 3:00 AM, Walter Bright wrote:
 Not that this is necessarily a bad thing, as I also promote the 
 safe/unsafe code dichotomy.
And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
http://plv.mpi-sws.org/rustbelt/
Thanks for the link. The project aims to the problem I've mentioned above and can really have a big impact.
Nov 07
prev sibling parent reply Paolo Invernizzi <paolo.invernizzi gmail.com> writes:
On Thursday, 7 November 2019 at 09:41:05 UTC, Timon Gehr wrote:
 On 07.11.19 08:34, drug wrote:
 On 11/7/19 3:00 AM, Walter Bright wrote:
 Not that this is necessarily a bad thing, as I also promote 
 the safe/unsafe code dichotomy.
And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
http://plv.mpi-sws.org/rustbelt/
"... Any realistic languages targeting this domain in the future will encounter the same problem ..." I underline _realistic_ ... Sorry Walter, I'm all with Timon on that.
Nov 07
next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/7/2019 7:34 AM, Paolo Invernizzi wrote:
 On Thursday, 7 November 2019 at 09:41:05 UTC, Timon Gehr wrote:
 On 07.11.19 08:34, drug wrote:
 On 11/7/19 3:00 AM, Walter Bright wrote:
 Not that this is necessarily a bad thing, as I also promote the safe/unsafe 
 code dichotomy.
And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
http://plv.mpi-sws.org/rustbelt/
"... Any realistic languages targeting this domain in the future will encounter the same problem ..." I underline _realistic_  ... Sorry Walter, I'm all with Timon on that.
I don't see anything on that site that contradicts what I wrote. In particular: "Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art." is saying the same thing.
Nov 07
next sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 08.11.19 04:43, Walter Bright wrote:
 On 11/7/2019 7:34 AM, Paolo Invernizzi wrote:
 On Thursday, 7 November 2019 at 09:41:05 UTC, Timon Gehr wrote:
 On 07.11.19 08:34, drug wrote:
 On 11/7/19 3:00 AM, Walter Bright wrote:
 Not that this is necessarily a bad thing, as I also promote the 
 safe/unsafe code dichotomy.
And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
http://plv.mpi-sws.org/rustbelt/
"... Any realistic languages targeting this domain in the future will encounter the same problem ..." I underline _realistic_  ... Sorry Walter, I'm all with Timon on that.
I don't see anything on that site that contradicts what I wrote. In particular: "Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art." is saying the same thing.
Indeed, but more importantly, this group is working on verification techniques for unsafe Rust code, so it is likely that unsafe Rust libraries will be proved correct in the future. There is also this recent work on functional verification of safe Rust code: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:prusti.pdf
Nov 08
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/8/2019 2:09 AM, Timon Gehr wrote:
 On 08.11.19 04:43, Walter Bright wrote:
 I don't see anything on that site that contradicts what I wrote. In particular:

 "Rust's core type system prohibits the aliasing of mutable state, but this is 
 too restrictive for implementing some low-level data structures. Consequently, 
 Rust's standard libraries make widespread internal use of "unsafe" blocks, 
 which enable them to opt out of the type system when necessary. The hope is 
 that such "unsafe" code is properly encapsulated, so that Rust's 
 language-level safety guarantees are preserved. But due to Rust's reliance on 
 a weak memory model of concurrency, along with its bleeding-edge type system, 
 verifying that Rust and its libraries are actually safe will require 
 fundamental advances to the state of the art."

 is saying the same thing.
Indeed, but more importantly, this group is working on verification techniques for unsafe Rust code, so it is likely that unsafe Rust libraries will be proved correct in the future.
I read it as ensuring the interface to the unsafe code is correct, not the unsafe code itself. I.e. "is properly encapsulated". After all, if the unsafe code can be proved correct, then it is no longer unsafe, and Rust's ownership/borrowing system can be dispensed with entirely as unnecessary for safety. I'm happy to let the CS Phd's work on those problems, as I am way out of my depth on it. I've convinced myself that the Ownership/Borrowing notion is sound, but have no idea how to formally prove it.
 There is also this recent work on functional verification of safe Rust code: 
 http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:prusti.pdf
I don't see any reason why the techniques used in the paper wouldn't work on D, given O/B. Note that the paper says: "We do not address unsafe code in this paper".
Nov 08
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 8 November 2019 at 10:25:44 UTC, Walter Bright wrote:
 After all, if the unsafe code can be proved correct, then it is 
 no longer unsafe, and Rust's ownership/borrowing system can be 
 dispensed with entirely as unnecessary for safety.
They probably mean that it is verified with human provided guides. A human must annotate the library with carefully chosen asserts that the verifier will prove one-by-one until they can all be disposed of. So you have to understand that verification engine and carefully "nudge" it until it succeeds. So, mostly suitable for the standard library and simple third party libraries, but not for bleeding-edge applications that keep changing...
Nov 08
prev sibling next sibling parent Timon Gehr <timon.gehr gmx.ch> writes:
On 08.11.19 11:25, Walter Bright wrote:
 On 11/8/2019 2:09 AM, Timon Gehr wrote:
 On 08.11.19 04:43, Walter Bright wrote:
 I don't see anything on that site that contradicts what I wrote. In 
 particular:

 "Rust's core type system prohibits the aliasing of mutable state, but 
 this is too restrictive for implementing some low-level data 
 structures. Consequently, Rust's standard libraries make widespread 
 internal use of "unsafe" blocks, which enable them to opt out of the 
 type system when necessary. The hope is that such "unsafe" code is 
 properly encapsulated, so that Rust's language-level safety 
 guarantees are preserved. But due to Rust's reliance on a weak memory 
 model of concurrency, along with its bleeding-edge type system, 
 verifying that Rust and its libraries are actually safe will require 
 fundamental advances to the state of the art."

 is saying the same thing.
Indeed, but more importantly, this group is working on verification techniques for unsafe Rust code, so it is likely that unsafe Rust libraries will be proved correct in the future.
I read it as ensuring the interface to the unsafe code is correct, not the unsafe code itself. I.e. "is properly encapsulated". ...
Read the next sentence after that. In general, feel free to read it any way you like, but that's not going to change the goals of the project, which correspond to my summary. https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf Last sentences in abstract: "Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem."
 After all, if the unsafe code can be proved correct, then it is no 
 longer unsafe, and Rust's ownership/borrowing system can be dispensed 
 with entirely as unnecessary for safety.
 ...
That stance makes little sense. The proofs are manual. As an analogy, it's a bit like saying "if it is realistic to audit trusted functions, we can just mark the entire codebase trusted, obtaining memory safe code without any of the safe restrictions". The difference is that here, the proofs can be checked by the computer, but that doesn't make them much easier to provide.
 I'm happy to let the CS Phd's work on those problems, as I am way out of 
 my depth on it.
 ...
I understand, but I can't help but notice that you often choose to contradict what they are saying on those issues anyway. The bird's-eye perspective you would get from an understanding of program verification and dependent type theory would help a lot for the design of sound and expressive type system extensions, such as O/B for D.
 I've convinced myself that the Ownership/Borrowing notion is sound, but 
 have no idea how to formally prove it.
 ...
One way is to embed it into separation logic. It's in the paper below.
 There is also this recent work on functional verification of safe Rust 
 code: 
 http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?med
a=papers:prusti.pdf 
I don't see any reason why the techniques used in the paper wouldn't work on D,
Indeed, separation logic "works" on any language: https://vst.cs.princeton.edu/download/VC.pdf https://vst.cs.princeton.edu/veric/ The reason why you want both safe and system code is that most programmers are unable or unwilling to manually carry out memory safety proofs for all the code they write.
 given O/B.
 ...
Sure. Given O/B of the same caliber, you would get a similar simplification of correctness proofs. But right now we don't have correctness proofs at all, and a lot of times when program verification came up on this newsgroup it was rejected with a vague reference to the halting problem.
 Note that the paper says: "We do not address unsafe code in this paper".
(I'm aware, having read the paper. Which is of course why I described it as "functional verification of _safe_ Rust code". They also refer to RustBelt for verification of unsafe code.)
Nov 08
prev sibling parent reply Doc Andrew <x x.com> writes:
On Friday, 8 November 2019 at 10:25:44 UTC, Walter Bright wrote:
 
 Indeed, but more importantly, this group is working on 
 verification techniques for unsafe Rust code, so it is likely 
 that unsafe Rust libraries will be proved correct in the 
 future.
I read it as ensuring the interface to the unsafe code is correct, not the unsafe code itself. I.e. "is properly encapsulated". After all, if the unsafe code can be proved correct, then it is no longer unsafe, and Rust's ownership/borrowing system can be dispensed with entirely as unnecessary for safety. I'm happy to let the CS Phd's work on those problems, as I am way out of my depth on it. I've convinced myself that the Ownership/Borrowing notion is sound, but have no idea how to formally prove it.
 There is also this recent work on functional verification of 
 safe Rust code: 
 http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:prusti.pdf
I don't see any reason why the techniques used in the paper wouldn't work on D, given O/B. Note that the paper says: "We do not address unsafe code in this paper".
The AdaCore/SPARK folks have done a lot of related work here that might be useful: https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memory-Management-in-Ada-and-SPARK.pdf They took the pointer borrowing idea from Rust and plugged it into the SPARK solver (Why3) so formal correctness is guaranteed. I am very bullish on formal verification in languages going forward. The one big advantage that D has in this arena is DbC. I was disappointed in your NWCPP talk that you listed it as a "miss." :) The potential here is huge! I think it's entirely possible that we can do _compile-time_ proofs that D contracts can be satisfied. With sufficient pre & post-conditions on "unsafe" functions, (and maybe, as somebody pointed out, some asserts along the way to "nudge" the solver in the right direction), you can prove at that nothing bad happens with an automated solver. A couple of other contract types like loop & type invariants might also be necessary (they are in SPARK, at least). It would be pretty cool if you had to mark a function as unsafe only if the compiler (with some help) couldn't prove otherwise. If Rust is going the route of a team of pros doing manual proofs in Coq to demonstrate absence of errors in "unsafe" code, they're in for a world of pain, frankly. My understanding is that the formal verification efforts in Rust were more geared towards proving that the Rust language/compiler themselves were sound, rather than giving Rust users a way of proving correctness of their own code, but I may be mistaken. The paper you linked shows the opposite, though. I'm not an expert, and it's only a hunch, but I suspect that DbC + CTFE could make formal verification of D code a lot easier to implement than trying to graft it on to other languages. The PhD students can tell me if I'm wrong :) My take is that formal verification is sort of where AI/ML was 20 years ago - academically interesting but of little practical use. Now it's a big deal, and I think in 10-20 years, FV will be too. -Doc
Nov 08
next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 8 November 2019 at 16:10:32 UTC, Doc Andrew wrote:
 With sufficient pre & post-conditions on "unsafe" functions, 
 (and maybe, as somebody pointed out, some asserts along the way 
 to "nudge" the solver in the right direction), you can prove at 
 that nothing bad happens with an automated solver.
If you talk only about memory safety and require that programs are written in a certain way, then maybe yes. In the general case this will not be possible though. You certainly need to manually guide the verifier (e.g. "nudge" the solver with asserts). The search space is vast. Keep in mind that when humans do proofs in math they do a lot of pattern matching, use a high level conceptualization of the problem space and only do it on "toy-sized" problems.
 I'm not an expert, and it's only a hunch, but I suspect that 
 DbC + CTFE could make formal verification of D code a lot 
 easier to implement than trying to graft it on to other 
 languages.
Formal verification is never easy, but certainly less difficult when the programming language is designed with that in mind... D is too flexible. And that's only for single-threaded programs. Add multi-threading and you basically need the programming language to be designed for it to get anywhere realistic. Such languages do exist, but they are not going to give you C-performance.
 My take is that formal verification is sort of where AI/ML was 
 20 years ago - academically interesting but of little practical 
 use. Now it's a big deal, and I think in 10-20 years, FV will 
 be too.
I think FV is where AI was 70 years ago... But yeah, maybe neural networks can be used for matching up verification problems with strategies so that the verifier succeeds more frequently, but the fact that an automated verifier frequently will fail to reach any conclusion will remain for practical programming that aim for very high performance in the forseeable future. A more likely future is that processing performance will be in abundance and that you therefore don't have to write programs that maximize performance and can switch to languages and algorithms that are easier to prove correct...
Nov 08
parent reply Doc Andrew <x x.com> writes:
On Friday, 8 November 2019 at 16:33:48 UTC, Ola Fosheim Grøstad 
wrote:
 On Friday, 8 November 2019 at 16:10:32 UTC, Doc Andrew wrote:
 With sufficient pre & post-conditions on "unsafe" functions, 
 (and maybe, as somebody pointed out, some asserts along the 
 way to "nudge" the solver in the right direction), you can 
 prove at that nothing bad happens with an automated solver.
If you talk only about memory safety and require that programs are written in a certain way, then maybe yes. In the general case this will not be possible though. You certainly need to manually guide the verifier (e.g. "nudge" the solver with asserts). The search space is vast. Keep in mind that when humans do proofs in math they do a lot of pattern matching, use a high level conceptualization of the problem space and only do it on "toy-sized" problems.
Sure, one reason SPARK is amenable to FV is because the language restrictions and richness of Ada types does a lot to restrict that search space, the same way dependently-typed languages do.
 I'm not an expert, and it's only a hunch, but I suspect that 
 DbC + CTFE could make formal verification of D code a lot 
 easier to implement than trying to graft it on to other 
 languages.
Formal verification is never easy, but certainly less difficult when the programming language is designed with that in mind... D is too flexible.
For sure - but there may be a _useful_ formally-verifiable subset of D buried in there somewhere, kind of like MISRA C.
 And that's only for single-threaded programs. Add 
 multi-threading and you basically need the programming language 
 to be designed for it to get anywhere realistic. Such languages 
 do exist, but they are not going to give you C-performance.
With the way we do multi-threading now, where anything goes, absolutely. SPARK can formally verify multi-threaded tasks but using a fairly restrictive model (Ravenscar). I don't think performance goes absolutely in the tank with Ravenscar, but yeah, if you don't worry about synchronization, ignore race conditions, and just hope for the best, then sure, you're going to win in the benchmarks :) I look at it a little differently - multi-threaded code is so tough to get right that some sort of verified correctness for it is becoming _essential_. (see: https://www.phoronix.com/scan.php?page=news_item&px=Google-KCSAN-Sanitizer) It may be that a slightly-different threading model, perhaps like that thread "nursery" idea which has been posted here before (https://vorpus.org/blog/notes-on-structured-concurrency-or-go-statement- onsidered-harmful/) will be a magic bullet... or not.
 My take is that formal verification is sort of where AI/ML was 
 20 years ago - academically interesting but of little 
 practical use. Now it's a big deal, and I think in 10-20 
 years, FV will be too.
I think FV is where AI was 70 years ago...
Way too pessimistic! :)
 But yeah, maybe neural networks can be used for matching up 
 verification problems with strategies so that the verifier 
 succeeds more frequently, but the fact that an automated 
 verifier frequently will fail to reach any conclusion will 
 remain for practical programming that aim for very high 
 performance in the forseeable future.
One thing that I've looked around for (without much luck) is just using GPUs to speed up the solvers themselves. Apparently parallelizing SAT solvers isn't the easiest thing in the world, but it would be a neat research topic.
 A more likely future is that processing performance will be in 
 abundance and that you therefore don't have to write programs 
 that maximize performance and can switch to languages and 
 algorithms that are easier to prove correct...
The cool thing is that, with the right proofs in place, you can actually get _faster_ code when formally verified, because all of the normal sanity-checks you do in code can get shifted to compile-time. You might even be able to reduce or eliminate thread blocking, etc. with the right model (and probably some HW assistance). Your point is well taken, but I do hope that we can get proven correctness of bare-metal code without having to write something like Liquid Haskell ;) -Doc
Nov 08
next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 8 November 2019 at 17:07:59 UTC, Doc Andrew wrote:
 With the way we do multi-threading now, where anything goes, 
 absolutely. SPARK can formally verify multi-threaded tasks but 
 using a fairly restrictive model (Ravenscar). I don't think 
 performance goes absolutely in the tank with Ravenscar, but 
 yeah, if you don't worry about synchronization, ignore race 
 conditions, and just hope for the best, then sure, you're going 
 to win in the benchmarks :)
Ok, so Ravenscar requires tasks to be dispatched in a FIFO manner, but you should be able to do better than that if you only get to use high level synchronization. For instance there are people who do verification of distributed communication protocols, so if you use some kind of message-passing scheme (or equivalent) then those approaches would apply.
 It may be that a slightly-different threading model, perhaps 
 like that thread "nursery" idea which has been posted here 
 before
«Structured concurrency» reminds me of rendezvous, i.e. that threads wait for each other at certain points, but less flexible. I'm not really convinced that a "nursery" is easier to deal with than futures/promises, in the general case, though.
 One thing that I've looked around for (without much luck) is 
 just using GPUs to speed up the solvers themselves. Apparently 
 parallelizing SAT solvers isn't the easiest thing in the world, 
 but it would be a neat research topic.
There are papers on it, but solvers are sensitive to the strategies (heuristics) used... so might be difficult to get right on a GPU. You'd probably have to use some kind of hybrid. I also see that there are papers on FPGA SAT solvers.
 The cool thing is that, with the right proofs in place, you can 
 actually get _faster_ code when formally verified, because all 
 of the normal sanity-checks you do in code can get shifted to 
 compile-time.
Sure, like indexing of arrays (array bounds checks).
 Your point is well taken, but I do hope that we can get proven 
 correctness of bare-metal code without having to write 
 something like Liquid Haskell ;)
Liquid Haskell looks interesting, though. You might find this interesting: http://leino.science/dafny-power-user/ It gives some hints of where such languages might go.
Nov 08
next sibling parent Doc Andrew <x x.com> writes:
On Friday, 8 November 2019 at 17:41:06 UTC, Ola Fosheim Grøstad 
wrote:
 Your point is well taken, but I do hope that we can get proven 
 correctness of bare-metal code without having to write 
 something like Liquid Haskell ;)
Liquid Haskell looks interesting, though. You might find this interesting: http://leino.science/dafny-power-user/ It gives some hints of where such languages might go.
Thanks for the link! I've looked briefly at Dafny in the past and liked what I saw. Between Dafny, F* and the Lean prover, MS research is doing some pretty neat work in the field.
Nov 08
prev sibling parent reply Sebastiaan Koppe <mail skoppe.eu> writes:
On Friday, 8 November 2019 at 17:41:06 UTC, Ola Fosheim Grøstad 
wrote:
 «Structured concurrency» reminds me of rendezvous, i.e. that 
 threads wait for each other at certain points, but less 
 flexible.
What I found insightful is the idea that without structured concurrency, functions can just spawn tasks with no obligation to wait or clean them up. What you find in practice is that those responsibilities are often spread over several functions. The result is that even if you have clean code, the end and start of those tasks is woven like spaghetti through your code. Structured concurrency introduces blocks for concurrency, which are similar to those introduced by structured programming. You can always be sure that when a nursery is exited, all its tasks have properly ended. I for one have had many occasions where I had a rogue task or a leaking websocket. With structured concurrency writing that code is easier, but more importantly, reviewing is easier as well.
 I'm not really convinced that a "nursery" is easier to deal 
 with than futures/promises, in the general case, though.
You still have futures with a nursery. It is just that you can't leave the nursery block without all concurrent tasks completing, timing out or being canceled.
Nov 08
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 8 November 2019 at 20:28:32 UTC, Sebastiaan Koppe 
wrote:
 I for one have had many occasions where I had a rogue task or a 
 leaking websocket.

 With structured concurrency writing that code is easier, but 
 more importantly, reviewing is easier as well.
Right, code with multiple futures can look a bit messy as the management of different futures and the main flow often ends up being interleaved in the source code.
 You still have futures with a nursery. It is just that you 
 can't leave the nursery block without all concurrent tasks 
 completing, timing out or being canceled.
So one can easily build something nursery-like on top of a futures-library that provide a wait_for_all(…) function, or like OS-X dispatch queues with dispatch_group_wait(…). I can see how that could be useful sometimes, for sure.
Nov 08
prev sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 8 November 2019 at 17:07:59 UTC, Doc Andrew wrote:
 For sure - but there may be a _useful_ formally-verifiable 
 subset of D buried in there somewhere, kind of like MISRA C.
I guess it is worth mentioning though that all integers in D follow the semantics of modular math, so you would not be able to conduct proofs with the assumption that you work with natural integers. So you cannot assume that "x+1 > x" for any type in D, that might make many proofs more difficult. Modular math can be handled with bit-blasting (turning each bit to a logic expression and use SAT), but maybe with less success.
Nov 08
parent reply Doc Andrew <x x.com> writes:
On Friday, 8 November 2019 at 17:55:41 UTC, Ola Fosheim Grøstad 
wrote:
 On Friday, 8 November 2019 at 17:07:59 UTC, Doc Andrew wrote:
 For sure - but there may be a _useful_ formally-verifiable 
 subset of D buried in there somewhere, kind of like MISRA C.
I guess it is worth mentioning though that all integers in D follow the semantics of modular math, so you would not be able to conduct proofs with the assumption that you work with natural integers. So you cannot assume that "x+1 > x" for any type in D, that might make many proofs more difficult. Modular math can be handled with bit-blasting (turning each bit to a logic expression and use SAT), but maybe with less success.
It works if you explicitly mark overflow as an error. You can try to prove that x <= x.max for a given path, and if you can't, then you just flag a warning. That's what SPARK does, at least. If the modular arithmetic is desired you'd probably have to manually put the overflow check and reassignment to 0 (or whatever) in there. That's one kind of annoying thing I discovered about Rust when working on some crypto code - having to write Wrapping types all over the place. The bad thing there was that the overflow checks were only in Debug mode, so in Release mode the code worked as intended without Wrapping. That was a few years ago, so things may be a little different now.
Nov 08
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 8 November 2019 at 18:11:39 UTC, Doc Andrew wrote:
 It works if you explicitly mark overflow as an error. You can 
 try to prove that x <= x.max for a given path, and if you 
 can't, then you just flag a warning.
So you manually assert it then? I guess you could use a templated type with asserts builtin. But then the solver have to figure out when to designate the type as an integer and when to designate it as a bitvector. I guess there is some room for that... perhaps. Another approach is to first prove the code correct for natural numbers and then try to prove that there is some upper limit and select an integer size that can contain that upper limit (e.g. 64 bits vs 32 bits). I am not sure about Dafny, but I think Whiley backends do that.
Nov 08
parent reply Doc Andrew <x x.com> writes:
On Friday, 8 November 2019 at 18:25:02 UTC, Ola Fosheim Grøstad 
wrote:
 On Friday, 8 November 2019 at 18:11:39 UTC, Doc Andrew wrote:
 It works if you explicitly mark overflow as an error. You can 
 try to prove that x <= x.max for a given path, and if you 
 can't, then you just flag a warning.
So you manually assert it then? I guess you could use a templated type with asserts builtin. But then the solver have to figure out when to designate the type as an integer and when to designate it as a bitvector. I guess there is some room for that... perhaps. Another approach is to first prove the code correct for natural numbers and then try to prove that there is some upper limit and select an integer size that can contain that upper limit (e.g. 64 bits vs 32 bits). I am not sure about Dafny, but I think Whiley backends do that.
With SPARK you don't have to manually assert the checks, it does the overflow checks as part of it's proof automatically. The neat thing is that you define new modular types with their range of allowable values, so as you prove the code, you show that those bounds aren't exceeded. It's basically a type invariant contract as part of the type definition itself (as I understand it).
Nov 08
next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 8 November 2019 at 18:39:25 UTC, Doc Andrew wrote:
 With SPARK you don't have to manually assert the checks, it 
 does the overflow checks as part of it's proof automatically. 
 The neat thing is that you define new modular types with their 
 range of allowable values, so as you prove the code, you show 
 that those bounds aren't exceeded. It's basically a type 
 invariant contract as part of the type definition itself (as I 
 understand it).
Hm, seems to me that it has signed integers with bounds that are non-modular and unsigned integers that are modular: https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html#integers So, in that case a prover could model bounded integers as integers with a constraint, and modular unsigned integers as bitvectors.
Nov 08
parent reply Doc Andrew <x x.com> writes:
On Friday, 8 November 2019 at 18:51:42 UTC, Ola Fosheim Grøstad 
wrote:
 On Friday, 8 November 2019 at 18:39:25 UTC, Doc Andrew wrote:
 With SPARK you don't have to manually assert the checks, it 
 does the overflow checks as part of it's proof automatically. 
 The neat thing is that you define new modular types with their 
 range of allowable values, so as you prove the code, you show 
 that those bounds aren't exceeded. It's basically a type 
 invariant contract as part of the type definition itself (as I 
 understand it).
Hm, seems to me that it has signed integers with bounds that are non-modular and unsigned integers that are modular: https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html#integers So, in that case a prover could model bounded integers as integers with a constraint, and modular unsigned integers as bitvectors.
I'm WAAAYYY out of my pay grade here, but I _think_ the distinction may depend on the underlying logic that the solver is using. Something like Coq where your Naturals are built on successor types would probably have a hard time with the modular arithmetic, but it might just not be a big deal for the Why3 solvers which I _think_ are using Hoare logic, since that's what HOL/ML is built on. I'm not really an expert in the Hoare logic though, and know just enough Coq to embarrass myself :) The Why3 solver will also let you use Coq to do a manual proof in the event that the automated prover can't figure it out, so I can't say for sure.
Nov 08
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 8 November 2019 at 19:04:38 UTC, Doc Andrew wrote:
 I'm not really an expert in the Hoare logic though
Roughly; Hoare logic is a set of rules for going from the precondition to the postcondition over a single statement. Each rule specify what the post condition should be given the precondition (and vice versa).
 myself :) The Why3 solver will also let you use Coq to do a 
 manual proof in the event that the automated prover can't 
 figure it out, so I can't say for sure.
Hm, that's interesting. I've bookmarked Why3, now… 4 l8r… :-)
Nov 08
parent Doc Andrew <x x.com> writes:
On Friday, 8 November 2019 at 19:11:52 UTC, Ola Fosheim Grøstad 
wrote:
 On Friday, 8 November 2019 at 19:04:38 UTC, Doc Andrew wrote:
 I'm not really an expert in the Hoare logic though
Roughly; Hoare logic is a set of rules for going from the precondition to the postcondition over a single statement. Each rule specify what the post condition should be given the precondition (and vice versa).
 myself :) The Why3 solver will also let you use Coq to do a 
 manual proof in the event that the automated prover can't 
 figure it out, so I can't say for sure.
Hm, that's interesting. I've bookmarked Why3, now… 4 l8r… :-)
I think we've probably given the next batch of GSoC candidates something to think about at least, haha.
Nov 08
prev sibling parent reply Doc Andrew <x x.com> writes:
On Friday, 8 November 2019 at 18:39:25 UTC, Doc Andrew wrote:
 On Friday, 8 November 2019 at 18:25:02 UTC, Ola Fosheim Grøstad 
 wrote:
 On Friday, 8 November 2019 at 18:11:39 UTC, Doc Andrew wrote:
 It works if you explicitly mark overflow as an error. You can 
 try to prove that x <= x.max for a given path, and if you 
 can't, then you just flag a warning.
So you manually assert it then? I guess you could use a templated type with asserts builtin. But then the solver have to figure out when to designate the type as an integer and when to designate it as a bitvector. I guess there is some room for that... perhaps. Another approach is to first prove the code correct for natural numbers and then try to prove that there is some upper limit and select an integer size that can contain that upper limit (e.g. 64 bits vs 32 bits). I am not sure about Dafny, but I think Whiley backends do that.
With SPARK you don't have to manually assert the checks, it does the overflow checks as part of it's proof automatically. The neat thing is that you define new modular types with their range of allowable values, so as you prove the code, you show that those bounds aren't exceeded. It's basically a type invariant contract as part of the type definition itself (as I understand it).
It's probably worth noting too that SPARK just translates the type definitions it sees into Why3 ML code, and uses that in the Why3 meta-solver for the proof. It separates proof from compilation, so if the proof checks out, then you can compile into bare-metal machine-code. This is a little different than a lot of the FV languages which take an ML/FP-ish language (with GC, etc.) and then have a C backend for it (with a runtime, usually).
Nov 08
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Friday, 8 November 2019 at 18:53:49 UTC, Doc Andrew wrote:
 It's probably worth noting too that SPARK just translates the 
 type definitions it sees into Why3 ML code, and uses that in 
 the Why3 meta-solver for the proof.
Ah, got it :) I haven't looked at Why3 yet.
 This is a little different than a lot of the FV languages which 
 take an ML/FP-ish language (with GC, etc.) and then have a C 
 backend for it (with a runtime, usually).
Yeah, high level FV languages can just do like Python and have unbounded integers and such.
Nov 08
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/8/2019 8:10 AM, Doc Andrew wrote:
 I am very bullish on formal verification in languages going forward. The one
big 
 advantage that D has in this arena is DbC. I was disappointed in your NWCPP
talk 
 that you listed it as a "miss." :) The potential here is huge! I think it's 
 entirely possible that we can do _compile-time_ proofs that D contracts can be 
 satisfied.
assert()s are the contracts that matter, not the in and out contracts, which can be replaced with assert()s. In no way did I mean to imply that assert()s were a mistake! I've thought for 35 years that assert()s can be the input to a program prover, i.e. it's nothing new, but I do not have the expertise to figure out such proofs might work, other than simplistic cases.
Nov 08
next sibling parent reply rikki cattermole <rikki cattermole.co.nz> writes:
On 09/11/2019 11:41 AM, Walter Bright wrote:
 
 I've thought for 35 years that assert()s can be the input to a program 
 prover, i.e. it's nothing new, but I do not have the expertise to figure 
 out such proofs might work, other than simplistic cases.
Sounds like some universities need to be contacted, perhaps a future PHD student would be interested in doing the theory.
Nov 08
next sibling parent reply Doc Andrew <x x.com> writes:
On Saturday, 9 November 2019 at 02:18:41 UTC, rikki cattermole 
wrote:
 Sounds like some universities need to be contacted, perhaps a 
 future PHD student would be interested in doing the theory.
It could be done in baby steps, too - maybe start with a tool that just shows no bad behavior occurs in a simple expression. Then show the same for entire pure functions. From there someone could work up to proving that pre/post-conditions in pure functions are satisfied. Then maybe go on to do invariants, then work up to safe nogc code, and so on. -Doc
Nov 08
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Saturday, 9 November 2019 at 02:55:37 UTC, Doc Andrew wrote:
 It could be done in baby steps, too - maybe start with a tool 
 that just shows no bad behavior occurs in a simple expression.
Exactly right. PREREQUISITE: Add something like «assume» to the language and make the optimizer add those to its fact database. For LLVM this should be trivial. Then add «assume» clauses to the standard library that are manually proven correct and also add an option to convert assume to assert for additional unit-testing. This allows you to get started working on the optimizer and figure out how to make good use of the extra facts. Also, optimizing the standard library affects all compiled programs... so even small gains might be worthwhile. STAGE 2: Add ensure-statements to the language. Those will be converted to assume-statements if you throw a switch, but display a warning that all ensure-statements have to be proven correct by an external verifier before compilation. Thus the entire burden has been moved to an external tool. This would encourage third parties to work on tools to translate D code into verifiable code to be consumed by standard verification tooling. Extension: create an online certification service that allows library code to carry a certificate that the library code has been verified. So that all their ensure statements can be turned into assume without throwing a switch. Certificates can be revoked (in case you find a bug in the verification process). STAGE 3: Then break all dynamic checks out as asserts by transforming the code. So that all bounds checks turn up as asserts. Break composite asserts into individual asserts. Verifying individual functions: step 1.1: use data-flow to convert as many asserts as possible into assumes step 1.2: use an external verifier to prove others if possible If those fail, try to do the verification at the call site: step 2.1: create a unique copy of the function for the call site step 2.2: use dataflow to bring additional assumed preconditions into the called function step 2.3: go to step 1.1
 Then show the same for entire  pure functions. From there 
 someone could work up to proving that pre/post-conditions in 
  pure functions are satisfied. Then maybe go on to do 
 invariants, then work up to  safe  nogc code, and so on.
Yup, start with the easy ones. Like pure functions provided as parameters to functions that work on arrays which often. Could even limit it to the ones used in the standard library.
Nov 09
parent reply Doc Andrew <x x.com> writes:
On Saturday, 9 November 2019 at 11:19:08 UTC, Ola Fosheim Grøstad 
wrote:
 PREREQUISITE:

 Add something like «assume» to the language and make the 
 optimizer add those to its fact database. For LLVM this should 
 be trivial.
As a stop-gap we might be able to use an assume UDA, but I do think "assume" could be added as a reserved keyword in the near future in anticipation...
 Then add «assume» clauses to the standard library that are 
 manually proven correct and also add an option to convert 
 assume to assert for additional unit-testing.
I like the idea of having a compiler flag to treat assumes as asserts, maybe even in release mode?
 This allows you to get started working on the optimizer and 
 figure out how to make good use of the extra facts.
That's probably a much longer-term goal, but just being able to move normal error-checking into contracts and depending on them in release code is a big win IMO.
 Also, optimizing the standard library affects all compiled 
 programs... so even small gains might be worthwhile.


 STAGE 2:

 Add ensure-statements to the language. Those will be converted 
 to assume-statements if you throw a switch, but display a 
 warning that all ensure-statements have to be proven correct by 
 an external verifier before compilation. Thus the entire burden 
 has been moved to an external tool.
This might be more difficult to enforce without some tight compiler integration. An attribute like ensured or certified could be the "gold standard" of safe D code, which would require a proof of no run-time errors and all contracts. Without the proof, the compiler could throw an error for functions with this attribute. Or, just treat it as a UDA and let the proof be a separate thing and let the user sort it all out. SPARK does the latter, but I like the idea of better compiler integration and support. We'd probably need a DIP to hash this out.
 This would encourage third parties to work on tools to 
 translate D code into verifiable code to be consumed by 
 standard verification tooling.

 Extension: create an online certification service that allows 
 library code to carry a certificate that the library code has 
 been verified. So that all their ensure statements can be 
 turned into assume without throwing a switch. Certificates can 
 be revoked (in case you find a bug in the verification process).
This might tie in with some of the work going on with reproducible builds, but I love the idea of certs for known good object files. Could you use a Merkle tree built-up by the compiler? So the source file hashes are baked into the object file (maybe just have a special symbol), then executables would contain a hash of all the object hashes. This is sort of an ancillary project to FV but if we are talking high-integrity software, it might be an easy win and a cool feather in D's cap.
 STAGE 3:

 Then break all dynamic checks out as asserts by transforming 
 the code. So that all bounds checks turn up as asserts. Break 
 composite asserts into individual asserts.
Using something like the certified (or ensured, or verified, or whatever) attribute, we could just turn off run-time checks in these functions if a proof exists, could be as simple as a source.d.proof file with the function name (and hash?) in it.
 Verifying individual functions:
 step 1.1: use data-flow to convert as many asserts as possible 
 into assumes
I'm not sure about this one. Usually assumes are big red flags, they're the FV version of unsafe - "trust me, I know what I'm doing", that sort of thing. I might have misunderstood your intent here though.
 step 1.2: use an external verifier to prove others if possible

 If those fail, try to do the verification at the call site:
 step 2.1: create a unique copy of the function for the call site
 step 2.2: use dataflow to bring additional assumed 
 preconditions into the called function
 step 2.3: go to step 1.1
This is how SPARK works, even if you can't prove a (normal Ada) function body, because of inline asm, or pointer arithmetic or something, you can still specify pre and post-contracts on the interface. I think there's a little bit of a trusted feel to it, since the post-conditions on a non-SPARK function become sort of an assumption that the function does what it claims, given the preconditions hold. I think SPARK may leave these as run-time checks (normal Ada behavior, normal D _Debug_ behavior), which you'd have to do to have any sort of confidence in your proof. This is where things get a little messy. Verified functions calling non-verified functions with post-condition checks would need these checks enabled even in release mode, I would think. The cool thing is that D _today_ has all the syntax it needs to start working on tooling for this with no language changes. Short-term, it may be of some benefit to reserve a couple keywords like assume or ensure, maybe set aside some attributes like verified or certified or ensured. Medium term, allowing invariant blocks to be associated with specific loops would probably be needed, maybe some extra compiler support for ensuring the presence of proofs. Longer term, I really like the idea of a "trusted language base" with certificates and object hashes that a maintainer can use to ensure complete accounting of everything that went into a particular build. I'm not as concerned as some are with proven builds and linking, but there may be high-integrity requirements in the future where this sort of thing is required. I'm not sure if it's a thing yet, maybe NASA does it, but I'd be surprised if anybody else is yet. All it takes is a high-profile case of somebody's cloud CI pipeline being compromised to use a malicious library, and everybody is going to be jumping on this sort of thing. It may be worth a DIP or a DConf session or something to hash out some of the long-term vision, but I think it's possible to start working on tools now. I'm not totally familiar with the landscape, but generating Why3ML from D seems like it would be one good way to start. You get access to a lot of solvers for free, it seems like it's well-documented and fairly easy to use. -Doc
Nov 09
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Saturday, 9 November 2019 at 14:49:32 UTC, Doc Andrew wrote:
 As a stop-gap we might be able to use an
  assume UDA, but I do think "assume" could be added as a 
 reserved keyword in the near future in anticipation...
True, I meant to refer to the concept, not syntax. Maybe the syntax for assume should be ugly enough to really stand out so that it is caught in reviews, " ASSUME" or " __assume"... Dunno. That is a detail, though.
 I like the idea of having a compiler flag to treat assumes as 
 asserts, maybe even in release mode?
It could at least be useful in cases where you do exhaustive unit testing (test all combinations), then assume would be safe.
 This allows you to get started working on the optimizer and 
 figure out how to make good use of the extra facts.
That's probably a much longer-term goal, but just being able to move normal error-checking into contracts and depending on them in release code is a big win IMO.
Well, not necessarily, some C++ compilers support it. The problem is that you probably don't want to introduce too many auxiliary facts, as that would just slow down compilation with no gain (and perhaps even confuse a naive optimizer). Anyway, you should be able to add facts to LLVM by compiling a boolean expression and then assuming it to hold. But maybe the language syntax should allow you to select which propositions you want to propagate to the optimizer. Not sure if LLVM can express quantifiers though (forall/exists).
 This might be more difficult to enforce without some tight 
 compiler integration. An attribute like  ensured or  certified 
 could be the "gold standard" of safe D code, which would 
 require a proof of no run-time errors and all contracts. 
 Without the proof, the compiler could throw an error for 
 functions with this attribute.
Well, that might be an issue, if the ensure-statement is meant to help optimization then it could simply be omitted. If it is meant to help correctness then it could be translated into an assert if it isn't verified. But I guess one will have to distinguish the two cases somehow. Which is basically why I think trying to improve basic libraries with assume-statements and manual proofs is the best starting point. Then you get an idea for how it can affect optimization. You probably also want to bake into a certificate trust-building meta information, such as which verification method, and who did it and where, so that developers can specify constraints like "must be verified by service X using verifier Y or Z". Or open up for hand-verified code by developer Q or a specific organization (could be a URL to a public-key).
 We'd probably need a DIP to hash this out.
I will certainly read and comment on it, if you want to write one. You could start with specc'ing out a list of requirements?
 This might tie in with some of the work going on with 
 reproducible builds, but I love the idea of certs for known 
 good object files.
I actually meant source code only. You distribute the source code, but with certified "requires"/"assume"/"ensures" statements that is bound to the source code using cryptographic hashing and an online index (so that it can be checked or revoked). I guess one issue is that it has to be a standalone library (e.g. only depend on a specific version of the standard library) for this to work. Otherwise you would have to tie it to a specific certified version of all the libraries you depend on. But... I don't actually think that is a big deal, you typically would pre-verify basic libraries. You could use a simple concatenation for the hash with sorted filenames and some sentinel character sequence for separating files, e.g.: filename1, sep, file1, sep, filename2, sep, file2, sep, sep.
 Using something like the  certified (or  ensured, or  verified, 
 or whatever) attribute, we could just turn off run-time checks 
 in these functions if a proof exists, could be as simple as a 
 source.d.proof file with the function name (and hash?) in it.
I am actually not sure how this could be done well. Because you could have array accesses within a conditional expression. Maybe you'd actually have to annotate the indexing with some new syntax to tell the compiler that the access does not need bounds checks as it has been proven already to hold... So I guess this is an area that needs to be fleshed out with many examples. Anyway, it seems reasonable that a tool would take source code, verify it and emit an annotated version of the source code. Then less capable compilers could use the verified results. Most users are not going to write verifiable code themselves.
 I'm not sure about this one. Usually assumes are big red flags, 
 they're the FV version of unsafe - "trust me, I know what I'm 
 doing", that sort of thing. I might have misunderstood your 
 intent here though.
I think so, if they are proven to hold by a tool/compiler then they hold. Dataflow analysis is sufficient, when it succeeds, but will fail in many cases at it is a weak approach. However, it is also much faster than a proper solver. Basically just an optimization for performance reasons. But you also want to use assume manually sometimes when describing hardware registers (e.g. describing that bit 8-32 always are zero), or when something has been proven by hand and has a significant performance impact.
 This is how SPARK works, even if you can't prove a (normal Ada) 
 function body, because of inline asm, or pointer arithmetic or 
 something, you can still specify pre and post-contracts on the 
 interface. I think there's a little bit of a  trusted feel to 
 it, since the post-conditions on a non-SPARK function become 
 sort of an assumption that the function does what it claims, 
 given the preconditions hold. I think SPARK may leave these as 
 run-time checks (normal Ada behavior, normal D _Debug_ 
 behavior), which you'd have to do to have any sort of 
 confidence in your proof.
Yes, for typical SPARK use cases that seems reasonable.
 This is where things get a little messy. Verified functions 
 calling non-verified functions with post-condition checks would 
 need these checks enabled even in release mode, I would think.
Yes, this is where different goals may lead to different designs... so the challenge is to come up with something that can both support correctness and optimization without being extremely complicated in terms of syntax.
 The cool thing is that D _today_ has all the syntax it needs to 
 start working on tooling for this with no language changes.
Sure, you could also just define a dummy "ensures", "requires", whatever… function that takes a boolean as a parameter. With an empty body, or an assert.
 a particular build. I'm not as concerned as some are with 
 proven builds and linking, but there may be high-integrity 
 requirements in the future where this sort of thing is 
 required. I'm not sure if it's a thing yet, maybe NASA does it, 
 but I'd be surprised if anybody else is yet.
There are papers on proof-carrying-assembly code... Although the basic idea behind certification would be that you get to use the postconditions and assumes without having to run costly verification on your own machine. You might even see a commercial service with very strong provers and effective hardware.
 I'm not totally familiar with the landscape, but generating 
 Why3ML from D seems like it would be one good way to start. You 
 get access to a lot of solvers for free, it seems like it's 
 well-documented and fairly easy to use.
Perhaps Why3ML is a good choice, but I would've started with Boogie.
Nov 09
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Saturday, 9 November 2019 at 17:16:40 UTC, Ola Fosheim Grøstad 
wrote:
 Well, not necessarily, some C++ compilers support it.  The 
 problem is that you probably don't want to introduce too many 
 auxiliary facts, as that would just slow down compilation with 
 no gain (and perhaps even confuse a naive optimizer). Anyway, 
 you should be able to add facts to LLVM by compiling a boolean 
 expression and then assuming it to hold.
Maybe by doing something along the lines of: if ( !must_be_true ) { llvm.unreachable }
Nov 09
prev sibling parent reply Doc Andrew <x x.com> writes:
On Saturday, 9 November 2019 at 17:16:40 UTC, Ola Fosheim Grøstad 
wrote:
 Well, not necessarily, some C++ compilers support it.  The 
 problem is that you probably don't want to introduce too many 
 auxiliary facts, as that would just slow down compilation with 
 no gain (and perhaps even confuse a naive optimizer). Anyway, 
 you should be able to add facts to LLVM by compiling a boolean 
 expression and then assuming it to hold.

 But maybe the language syntax should allow you to select which 
 propositions you want to propagate to the optimizer. Not sure 
 if LLVM can express quantifiers though (forall/exists).
I'm pretty ignorant of how all that would all work, is there some sort of a standard way to give optimizers "hints" based on what the solver can show? I don't want to over-sell the potential performance gains. (Like Rust fans talking about how _theoretically_, Rust is much faster than C because of the lack of pointer aliasing, but the benchmarks just don't bear it out. (yet))
 But I guess one will have to distinguish the two cases somehow. 
 Which is basically why I think trying to improve basic 
 libraries with assume-statements and manual proofs is the best 
 starting point. Then you get an idea for how it can affect 
 optimization.
Oof. You're gonna have a hard time finding volunteers for that one. I think that's how projects like SeL4 do it though, translating C into HOL and then adding verification conditions manually. I want to say the SeL4 proofs are something like 10x the number of lines as the code itself. Working manual proofs can be kind of fun, like a puzzle, but I've read about some negative case studies where manually verified code had some incorrect assumptions in the proofs, or proved things that ended up being orthogonal to the desired outcome. It's murky.
 I will certainly read and comment on it, if you want to write 
 one. You could start with specc'ing out a list of requirements?
I'll take a look at the DIP author guidelines and start putting something together. I think it's worth the community's consideration if we can do this in a way that minimizes impact. As a long time mostly-lurker and D user, I don't have any credibility with compiler changes, so I don't want to be one of those guys who jumps in with a big DIP that tries to make Walter and all the other contributors jump through their ass. I was toying with the idea of 2 or more parts: start with a single DIP for "D Formal Verification Support" that maybe just describes which UDAs should be agreed upon for external proof tools to use, the behavior that should be expected when using contracts in those tools, and maybe a small set of changes to the language spec: - Universal quantification: The low-impact way would be to set aside an attribute forall or foreach, then figure out what tuple elements you'd need to generate a VC from them and how you'd tie them to a function, module, variable, etc. (Longer-term, consider a change to the language to create a foreach expression or add a new expression "forall" (or something). I would anticipate a lot of weeping and gnashing of teeth.) - Existential quantification: I think you can do this in a low-impact way is to set aside an attribute exists or forsome and sort out the UDA tuple spec that provers would use. Longer term, add an "exists" or "forsome" expression. - Loop invariants: Allow invariant{} blocks inside loop statements in addition to classes and structs. This is the only part of the DIP that I can foresee requiring a language change; I don't know any way of attaching a UDA to a statement. I _think_ this would be the only blocker. LATER ON: if there's interest and any promise, then we could look at making parts of Phobos verified, adding compiler support for provers, etc. in follow-on DIPs. A very powerful addition would be user-defined scalar types with their own invariants, but this is a BIG language change. (Even better would be strong subtypes, refinement types, or first-order types, but you can simulate them well enough with contracts in an invariant clause). A smaller language change would be to give invariant a parameter with a hypothetical or ghost variable and allow it on aliases: alias uint ShoeSize; invariant(ShoeSize T){ assert(T > 0); assert(T < 24); } void buyBiggerShoes(ShoeSize s){ Shoe t; t.size = s + 1; //Consider this line //Invariant asserts get run if in Debug mode, so hopefully during // unit-testing you tried it with s == 23. //During proof time, this would warn with something like: // "Cannot prove t.size < 24 (example: when s == 23) // Possible solution: add s to list of preconditions for buyNewSchoolShoes" // (this is almost exactly what SPARK gives) sendOrder(t); } Built-in types would have implied invariants, at least as far as proofs are concerned: invariant(int i){ assert(i <= int.max); assert(i >= int.min); } So it might be that this initial DIP could just focus on beefing up invariant{}? I'd welcome any more-informed thoughts on how to proceed and go through the DIP process, if there's interest!
 I actually meant source code only. You distribute the source 
 code, but with certified "requires"/"assume"/"ensures" 
 statements that is bound to the source code using cryptographic 
 hashing and an online index (so that it can be checked or 
 revoked).

 I guess one issue is that it has to be a standalone library 
 (e.g. only depend on a specific version of the standard 
 library) for this to work. Otherwise you would have to tie it 
 to a specific certified version of all the libraries you depend 
 on.

 But... I don't actually think that is a big deal, you typically 
 would pre-verify basic libraries. You could use a simple 
 concatenation for the hash with sorted filenames and some 
 sentinel character sequence for separating files, e.g.:  
 filename1, sep, file1, sep, filename2, sep, file2, sep, sep.


 I am actually not sure how this could be done well. Because you 
 could have array accesses within a conditional expression.
Flow analysis can sort that out, checking both branches of the conditional and making sure that contracts hold in every case.
 Maybe you'd actually have to annotate the indexing with some 
 new syntax to tell the compiler that the access does not need 
 bounds checks as it has been proven already to hold... So I 
 guess this is an area that needs to be fleshed out with many 
 examples.

 Anyway, it seems reasonable that a tool would take source code, 
 verify it and emit an annotated version of the source code. 
 Then less capable compilers could use the verified results.

 Most users are not going to write verifiable code themselves.
Ideally, it will be easy to run the proof tool on existing code as a sort of linter in addition to unit tests and other static analysis. The first time you see warnings like "Cannot prove abc is less than def (example: def = 255)" because you didn't consider edge cases, it opens your eyes to how proofs can really save you from a lot of testing and debugging. The goal is that a user doesn't have to do anything different than normal to write verifiable code. It's all verifiable, but it's up to the user how deep they want to go down the rabbit hole to prove functional correctness by adding a ton of contracts.
 I think so, if they are proven to hold by a tool/compiler then 
 they hold. Dataflow analysis is sufficient, when it succeeds, 
 but will fail in many cases at it is a weak approach. However, 
 it is also much faster than a proper solver. Basically just an 
 optimization for performance reasons.

 But you also want to use assume manually sometimes when 
 describing hardware registers (e.g. describing that bit 8-32 
 always are zero), or when something has been proven by hand and 
 has a significant performance impact.
One kind of neat thing that SPARK has is the ability to break volatile down into sub-categories like "Effective_Reads", where reading a value takes something off a UART, or "Effective_Writes", where writing to a hardware register has some effect on the system, and "Async_Readers/Writers" where some hardware will be accessing memory behind the scenes... now how that affects the state of a proof, I'm not totally sure.
 Yes, this is where different goals may lead to different 
 designs... so the challenge is to come up with something that 
 can both support correctness and optimization without being 
 extremely complicated in terms of syntax.
I'm not super smart on the optimization side of the house, my focus would be on correctness first and then let the optimization wizards extract what useful information they can from that.
 Sure, you could also just define a dummy "ensures", "requires", 
 whatever… function that takes a boolean as a parameter. With an 
 empty body, or an assert.
I'll have to give some thought to this.
 There are papers on proof-carrying-assembly code...

 Although the basic idea behind certification would be that you 
 get to use the postconditions and assumes without having to run 
 costly verification on your own machine.

 You might even see a commercial service with very strong 
 provers and effective hardware.
I think you'll see SaaS offerings like this in 10 years, kind of like big ML farms now. Proofs on big code bases can take a long time, definitely something you would want as part of an overnight build in a CI pipeline. Single file proofs can go pretty quick though, depending on how deep you let them search.
 Perhaps Why3ML is a good choice, but I would've started with 
 Boogie.
I hadn't heard of Boogie before, but it looks promising - It doesn't feel quite as mature as Why3, but the syntax looks a lot friendlier, for sure. So, having done no DMD compiler hacking myself, is the state of the "DMD as a library" mature enough now to where somebody could import dmd.compiler, get an AST and start figuring out VCs? A DIP without some sort of prototype tooling, even if primitive, is going to be pretty toothless, IMO. -Doc
Nov 09
next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Saturday, 9 November 2019 at 21:11:14 UTC, Doc Andrew wrote:
 I'm pretty ignorant of how all that would all work, is there 
 some sort of a standard way to give optimizers "hints" based on 
 what the solver can show?
I don't think so, but if you establish something that is to weak for verification it still can potentially be used for optimization.
 I don't want to over-sell the potential performance gains.
Of course not, you would have to provide actual examples. The "easy" gains would be from removing dynamic checks, but not so easy in reality. If it is easy then the optimizer can already do it using dataflow analysis. So figuring out "trivial" small examples where the optimizer fails by looking at generated assembly is a good starting point.
 - Universal quantification: The low-impact way would be to set 
 aside an attribute  forall or  foreach, then figure out what 
 tuple elements you'd need to generate a VC from them and how 
 you'd tie them to a function, module, variable, etc.
I was more thinking, what do you do if it fails? One cannot keep O(N) or O(N^2) asserts in the code as a dynamic check... :-/ I guess the easy solution is to require that "ensure" is fulfilled at compile time and not allow quantified expressions in asserts.
 (Longer-term, consider a change to the language to create a 
 foreach expression or add a new expression "forall" (or 
 something). I would anticipate a lot of weeping and gnashing of 
 teeth.)
I once added a unicode-token-layer to the dmd-lexer, and added alternative unicode math symbols to expressions. It only took a few hours. Modifying the lexer is a lot easier than expanding the parser. I think people who would write VC also would be familiar with math notation, so I one could just use that to avoid clashes. E.g. you could have a not-so-pretty ascii syntax and a unicode shorthand. Like: "∀" vs " vc_forall" Unicode tokens is really easy to do this way as you just can rewrite "∀" to " vc_forall" and "∃" to " vc_exists", so no major changes are needed to add unicode symbols.
 - Loop invariants: Allow invariant{} blocks inside loop 
 statements in addition to classes and structs. This is the only 
 part of the DIP that I can foresee requiring a language change; 
 I don't know any way of attaching a UDA to a statement. I 
 _think_ this would be the only blocker.
Proving loop progression and termination is very important, and not so easy. What some FV languages do is that they introduce ghost-variables for this (variables that are conceptually computed but not used for code generation). So basically you increment the ghost variable(s) every iteration and prove that there is a threshold for the value where the loop terminates. But it won't really change the language that is compiled. It only changes the language that is verified. So not an effective change. But verification will probably have to happen after template expansion... Not sure how to deal with that. Unless you want to verify templated code... which would be cool, but not sure of what roadblocks you would hit.
 (Even better would be strong subtypes, refinement types, or 
 first-order types, but you can simulate them well enough with 
 contracts in an invariant clause).
Lots of potential with more advanced typing... but prepare to be met with a lot of resistance for things that are actual language changes (things that can affect code gen and not only the verifier).
 A smaller language change would be to give invariant a 
 parameter with a hypothetical or ghost variable and allow it on 
 aliases:
Well, yes, but not necessarily a language change... As a start you could just define a local function "__vc_invariant" and treat it special by the verifier?
 I'd welcome any more-informed thoughts on how to proceed and go 
 through the DIP process, if there's interest!
I don't know enough about what makes a DIP succeed. What is common in other languages is to make a library/tool implementation first as proof of concept and then argue that it would be better as a language extension. So that probably is the better approach... But I don't know. But reserving the vocabulary makes a lot of sense. Then I would point to other languages, particularly FV languages, so that you reserve the most common terms " requires", " ensures", " forall", " exists" etc. But in a proof-of-concept you can just use "_vc_requires" or some other prefix.
 I am actually not sure how this could be done well. Because 
 you could have array accesses within a conditional expression.
Flow analysis can sort that out, checking both branches of the conditional and making sure that contracts hold in every case.
No, I meant how to express it syntactically in a way that allows you to distribute pre-verified code. (The point of having verification would be to cover those cases that standard flow analysis fail on.)
 analysis. The first time you see warnings like "Cannot prove 
 abc is less than def (example: def = 255)" because you didn't 
 consider edge cases, it opens your eyes to how proofs can 
 really save you from a lot of testing and debugging.
Yes, maybe that is a use case. If you write up something formal you ought to list such use-cases, and what they require.
 The goal is that a user doesn't have to do anything different 
 than normal to write verifiable code.
:-/ not possible though.
 One kind of neat thing that SPARK has is the ability to break 
 volatile down into sub-categories like "Effective_Reads", where 
 reading a value takes something off a UART, or 
 "Effective_Writes", where writing to a hardware register has 
 some effect on the system, and "Async_Readers/Writers" where 
 some hardware will be accessing memory behind the scenes... now 
 how that affects the state of a proof, I'm not totally sure.
IIRC, D does not provide volatile though... You have to use something intrinsics-like. So memory mapped registers are not types in D, it is dealt with as a memory fenced access-action...
 So, having done no DMD compiler hacking myself, is the state of 
 the "DMD as a library" mature enough now to where somebody 
 could import dmd.compiler, get an AST and start figuring out 
 VCs?
No idea. I think the major hurdle for you would be the templating. Maybe only deal with non-templated code, because then you can use one of the D parsers and rewrite the code with verification-annotations instead of modifying the actual compiler. For a proof-of-concept.
 A DIP without some sort of prototype tooling, even if 
 primitive, is going to be pretty toothless, IMO.
Yes. You could write something "informational". Then evolve it later. But you'll get feedback on whether there is any interest at all in the community? If there is no interest then it would not be possible to maintain it in the compiler either. Starting a discussion on the vocabulary might tell you something about what kind of support you can expect for your ideas.
Nov 09
parent reply Doc Andrew <x x.com> writes:
On Sunday, 10 November 2019 at 00:27:46 UTC, Ola Fosheim Grøstad 
wrote:
 - Universal quantification: The low-impact way would be to set 
 aside an attribute  forall or  foreach, then figure out what 
 tuple elements you'd need to generate a VC from them and how 
 you'd tie them to a function, module, variable, etc.
I was more thinking, what do you do if it fails? One cannot keep O(N) or O(N^2) asserts in the code as a dynamic check... :-/ I guess the easy solution is to require that "ensure" is fulfilled at compile time and not allow quantified expressions in asserts.
Yeah, you could make ensure work like assert but strictly for proofs and not at runtime, but I kind of like the idea that if you can't prove a check at compile-time, it still makes it into your Debug code for thorough testing. For the most part you're back to the status quo when a proof fails - you've got some unit tests to write, the checks will live in Debug code and they'll go away in Release code just like they do now. If the Debug performance hit is too onerous, then comment it out, or have a separate "proof-time assert". I'd have to think it through. The one thing I'm not sure about is the situation I hinted at where post-conditions are on an interface where the function body itself wasn't proven. In this case, maybe they just act like assumptions. I have to do some more homework here.
 I once added a unicode-token-layer to the dmd-lexer, and added 
 alternative unicode math symbols to expressions. It only took a 
 few hours. Modifying the lexer is a lot easier than expanding 
 the parser. I think people who would write VC also would be 
 familiar with math notation, so I one could just use that to 
 avoid clashes.

 E.g. you could have a not-so-pretty ascii syntax and a unicode 
 shorthand.

 Like:  "∀" vs " vc_forall"

 Unicode tokens is really easy to do this way as you just can 
 rewrite "∀" to " vc_forall" and "∃" to " vc_exists", so no 
 major changes are needed to add unicode symbols.
You're going to scare people off with that sorta stuff :)
 Proving loop progression and termination is very important, and 
 not so easy. What some FV languages do is that they introduce 
 ghost-variables  for this (variables that are conceptually 
 computed but not used for code generation).

 So basically you increment the ghost variable(s) every 
 iteration and prove that there is a threshold for the value 
 where the loop terminates.

 But it won't really change the language that is compiled. It 
 only changes the language that is verified. So not an effective 
 change.

 But verification will probably have to happen after template 
 expansion... Not sure how to deal with that.  Unless you want 
 to verify templated code... which would be cool, but not sure 
 of what roadblocks you would hit.
Yeeeah... I'm not sure how that is going to play out. I don't really know how contracts work with templated code currently. It could be that if the contracts appear in template code, then they just get copy-pasted into each new instantiation of the template, and life is good. The prover will do a ton of extra work re-proving the same thing for each new type, but who cares? And actually, you might discover that the perfectly generic function you wrote actually has a bunch of nasty corner cases lurking inside... I think you'd just have to wait until all the CTFE and template stuff is done before you start generating VCs. It might not be a deal-breaker, but that's speaking from ignorance, frankly.
 Lots of potential with more advanced typing... but prepare to 
 be met with a lot of resistance for things that are actual 
 language changes (things that can affect code gen and not only 
 the verifier).
Oh yeah, I'm not holding my breath for anything like that. Baby steps.
 Well, yes, but not necessarily a language change... As a start 
 you could just define a local function "__vc_invariant" and 
 treat it special by the verifier?
True, we might be able to just use a nested function with some contracts baked into it.
 If you write up something formal you ought to list such 
 use-cases, and what they require.


 The goal is that a user doesn't have to do anything different 
 than normal to write verifiable code.
:-/ not possible though.
Oh I dunno, aside from adding some extra contracts and avoiding certain language constructs* (like goto), not much really has to change for the average user to get some benefit from running the code through a proof tool, even if they could care less about stamping a function as "certified" or not. * Granted, those "certain language constructs" may end up being an insurmountable barrier, where the formally verifiable subset of D is stripped of so many features that it isn't really worth it. Too early to tell.
 But you'll get feedback on whether there is any interest at all 
 in the community? If there is no interest then it would not be 
 possible to maintain it in the compiler either.

 Starting a discussion on the vocabulary might tell you 
 something about what kind of support you can expect for your 
 ideas.
Let me mull it over a bit. I might start a separate thread where people can weigh in. The field is still pretty new [AI/ML 70 years ago ;) ], so it might be a good way to raise awareness and at least get people thinking about some of the possibilities for writing _real_ safe code.
Nov 09
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Sunday, 10 November 2019 at 02:51:53 UTC, Doc Andrew wrote:
 I think you'd just have to wait until all the CTFE and template 
 stuff is done before you start generating VCs. It might not be 
 a deal-breaker, but that's speaking from ignorance, frankly.
Also keep in mind that you have to deal with exceptions, so you have to introduce a lot of branching code (unless the verifier does that rewriting for you).
 Oh I dunno, aside from adding some extra contracts and avoiding 
 certain language constructs* (like goto), not much really has
You can allow gotos (at least the most common usage). Deal with it the same way you model exceptions.
 * Granted, those "certain language constructs" may end up being 
 an insurmountable barrier, where the formally verifiable subset 
 of D is stripped of so many features that it isn't really worth 
 it. Too early to tell.
Well, I think that modular ints is an issue that may make some cases harder, but I think most constructs can be modelled in a VC language. Still a lot of work.
Nov 10
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Sunday, 10 November 2019 at 13:39:23 UTC, Ola Fosheim Grøstad 
wrote:
 You can allow gotos (at least the most common usage). Deal with 
 it the same way you model exceptions.
https://www.google.com/search?q=transformation+goto+eliminiation
Nov 10
prev sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Saturday, 9 November 2019 at 21:11:14 UTC, Doc Andrew wrote:
 A DIP without some sort of prototype tooling, even if 
 primitive, is going to be pretty toothless, IMO.
A fun way to get started might be to create your own verified mini-language and compile it to D code and use that as a proof-of-concept.
Nov 09
parent reply Doc Andrew <x x.com> writes:
On Sunday, 10 November 2019 at 00:31:18 UTC, Ola Fosheim Grøstad 
wrote:
 A fun way to get started might be to create your own verified 
 mini-language and compile it to D code and use that as a 
 proof-of-concept.
So that brings up the question of which approach to use. The idea you mentioned there is how F* (or at least the subset "Low"), Coq, and probably some others I can't think of - do it. You write verified functional code, run it either through an automated solver or write proofs manually, and then "extract" a compile-able (basically C) or interpret-able (OCaml, Scheme, Haskell...) program in another language from it. For C, I think usually they target the CLight dialect of C, so they can use the CompCert verified compiler http://compcert.inria.fr/doc/index.html. The cool thing here is that you can basically guarantee that the assembly that's generated matches the specifications of the original code. I consider this approach the "Obsessive-Compulsive" method. This is for the programmer who just _knows_ that there's a compiler bug causing his code to be wrong. :) This is more suited towards the goal of a totally verified toolchain. (Side note: There's a certain, say, "academic" beauty in thinking that you've got "turtles all the way down" with a totally verified language and toolchain. But there's always going to be hardware bugs, cosmic rays, out-of-memory conditions, etc.) Personally, I'm less worried about what DMD, GCC or LDC might have gotten wrong than what _I_ goofed up in my own code, so this option isn't super appealing to me. Eventually, I'd love for my compiler, standard library, OS, etc. to be formally-verified. But... they're probably not going to be written in Coq or ML, if we're being honest. D or Rust? More probable - so we get to option 2: Option 2, taken by Dafny and SPARK (and I think FRAMA-C too, but don't quote me on that), is take the language you want (or at least something close), then generate an intermediate language that can be easily broken down into verification conditions to run through the solver. For formally-verified D, this is the route I'd want, because I like writing D! Writing a verified language that extracts to D is sort of a dead-end, in my opinion. It doesn't make people's D code any safer, and if I'm going to extract to a compiled language, then I might as well decide on C/CLight and take advantage of CompCert or some other toolchain that's been verified already, or just use GCC and get wider platform exposure. Option 3 is to just take the language as it is and try to generate some kind of formal logic based on the language constructs as you parse it, then work out the solver mechanics or some kind of proof assistant for working through it. There might be _somebody_ out there that could take this on, but it ain't me! A lot of smart people have already worked out automated provers for ML-ish languages, and D is unique in that it already has nice contract syntax that could map nicely to the axioms and verification conditions that those languages use. I suspect that ultimately, we could get what we need by taking some intermediate DMD front-end state (maybe AST + UDA __traits), doing flow analysis, and dumping out (a lot of) some intermediate verification language with the assertions baked in and run an existing proof tool on it. You'd have to do some gonkulation of the solver output to figure out what your original line of code was for sensible error messages, but that's possible. Microsoft's VCC multithreaded C verifier tool might be a good starting point, since it's got a friendly license (MIT) - https://github.com/microsoft/vcc. It uses Boogie, too. SPARK (the GNATProve tool, specifically) is all GPLed, so not sure if it's a good resource or not. IANAL and all that. That's an almost criminally-understated view of the task, but I think it might give D a path towards FV, if people think it's worth it. D has always been on the cutting edge of good SW engineering support in a language, so who knows? -Doc
Nov 09
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Sunday, 10 November 2019 at 04:15:08 UTC, Doc Andrew wrote:
 Option 2, taken by Dafny and SPARK (and I think FRAMA-C too, 
 but don't quote me on that), is take the language you want (or 
 at least something close), then generate an intermediate 
 language that can be easily broken down into verification 
 conditions to run through the solver.

 For formally-verified D, this is the route I'd want, because I 
 like writing D!
Sounds like you have set a course that you can follow! I would personally just have ignored templates and extended one of the linty D-parser, as I think it will lead to a more transparent codebase that is easier to experiment with than modifying the D compiler. But maybe you'll find that doing it within dmd from start works out for you. The plain dmd compiler should not so difficult to set up, so just try it, I guess? You could build your own VC-ast from the D-ast, then manipulate it and emit VC-code.
 That's an almost criminally-understated view of the task, but I 
 think it might give D a path towards FV, if people think it's 
 worth it.
Yes, I don't know, what is most important is that you think it is important enough to carry the burden on your own for at least a year. Over time, surely others will come along that share that viewpoint. Just keep the codebase simple so that people with no FV knowledge can contribute... In the beginning there will basically be no advantages to using the tool, so... it takes a lot of patience. Maybe a well written DIP can bring people on board from the start, but I haven't seen many people interested in FV when that topic has been discussed in the forums. Again, just try, I guess?
Nov 10
prev sibling next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Saturday, 9 November 2019 at 02:18:41 UTC, rikki cattermole 
wrote:
 Sounds like some universities need to be contacted, perhaps a 
 future PHD student would be interested in doing the theory.
Not sure what theory that would be. The basic idea is well known and pretty straight forward: 1. Try to prove that the assert holds by feeding the function into an external prover. 2. If it fails, retain the assert in the code or omit it. 3. If it succeeds, replace the assert with an «assume(…)» statement. 4. Compile. You can do this today if you want to. The challenge is to make sure that the optimizer will make good use of it.
Nov 09
prev sibling parent reply RazvanN <razvan.nitu1305 gmail.com> writes:
On Saturday, 9 November 2019 at 02:18:41 UTC, rikki cattermole 
wrote:
 On 09/11/2019 11:41 AM, Walter Bright wrote:
 
 I've thought for 35 years that assert()s can be the input to a 
 program prover, i.e. it's nothing new, but I do not have the 
 expertise to figure out such proofs might work, other than 
 simplistic cases.
Sounds like some universities need to be contacted, perhaps a future PHD student would be interested in doing the theory.
At UPB Bucharest we have discussed with a formal verification professor and published a research project for a masters student (2 years) where the goal is to implement a simple solver for contracts in D.
Nov 10
parent reply Doc Andrew <x x.com> writes:
On Sunday, 10 November 2019 at 10:53:38 UTC, RazvanN wrote:
 At UPB Bucharest we have discussed with a formal verification 
 professor and published a research project for a masters 
 student (2 years) where the goal is to implement a simple 
 solver for contracts in D.
Very cool! Do you know if there is a link or any publications (even if it's just a proposal) for the research? -Doc
Nov 10
parent RazvanN <razvan.nitu1305 gmail.com> writes:
On Sunday, 10 November 2019 at 20:02:33 UTC, Doc Andrew wrote:
 On Sunday, 10 November 2019 at 10:53:38 UTC, RazvanN wrote:
 At UPB Bucharest we have discussed with a formal verification 
 professor and published a research project for a masters 
 student (2 years) where the goal is to implement a simple 
 solver for contracts in D.
Very cool! Do you know if there is a link or any publications (even if it's just a proposal) for the research? -Doc
Unfortunately, I do not know the site where it has been published, but the proposal is in Romanian anyway. What I know is that the student will have to do a state of the art review in verification techniques and come up with a proposal. The milestones are: 1. State of the art review 2. Implement one of the existing techniques 3. Come up with an enhancement of some sort. We don't know yet the exact details, but we are confident that at least we can implement something that is already out there.
Nov 10
prev sibling next sibling parent reply Doc Andrew <x x.com> writes:
On Friday, 8 November 2019 at 22:41:23 UTC, Walter Bright wrote:
 assert()s are the contracts that matter, not the in and out 
 contracts, which can be replaced with assert()s. In no way did 
 I mean to imply that assert()s were a mistake!

 I've thought for 35 years that assert()s can be the input to a 
 program prover, i.e. it's nothing new, but I do not have the 
 expertise to figure out such proofs might work, other than 
 simplistic cases.
Now you've done it. I've seen this before, right before templates were in D. This is where you disappear for a couple of weeks and then come back to announce that D can formally verify user code, right? :) The in/out syntax doesn't add a lot for typical function body code, since everything is in sequential order anyhow, but in interfaces they would be essential. They may be under-utilized, but I think they might just be one of those features that is a late bloomer. I wouldn't consider taking them out of the language just yet, even for regular functions. Proving properties of D code outright is probably tough, but doing a mechanical conversion (of at least some subset of D, maybe betterC) to an intermediate language like ML and then feeding it into a solver is probably possible. Here's an interesting project I found that can generate Why code from LLVM-IR: https://github.com/AnnotationsForAll/WhyR. It might be interesting to throw some LDC IR at it and just see what happens! Given that D already has contracts in place, using them to generate Why's "ensures" and "requires" clauses would be much easier than something like C where you'd need specially-formatted comments or a language extension. Even without specific contracts, a list of things that you _know_ are run-time errors (divide-by-zero, null-pointer dereference, etc.) could be proven absent from code. The nice thing about an approach like this is that you don't have to change the language or mess with the compiler, instead the prover is just another tool, like a linter, that you can use if you need it. Not everybody is as optimistic as I am, but I do believe that with the emphasis on safety these days, I suspect FV will become a requirement in the future. -Doc
Nov 08
parent Walter Bright <newshound2 digitalmars.com> writes:
On 11/8/2019 6:43 PM, Doc Andrew wrote:
 Even without specific contracts, a list of things that you _know_ are run-time 
 errors (divide-by-zero, null-pointer dereference, etc.) could be proven absent 
 from code.
Actually, I deliberately insert null-pointer dereferences to get stack traces when debugging :-) Anyhow, don't worry, in/out contracts are remaining because some people do use them. There are some benefits to them, but I just don't think they're worth the cost.
Nov 09
prev sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 08.11.19 23:41, Walter Bright wrote:
 On 11/8/2019 8:10 AM, Doc Andrew wrote:
 I am very bullish on formal verification in languages going forward. 
 The one big advantage that D has in this arena is DbC. I was 
 disappointed in your NWCPP talk that you listed it as a "miss." :) The 
 potential here is huge! I think it's entirely possible that we can do 
 _compile-time_ proofs that D contracts can be satisfied.
assert()s are the contracts that matter, not the in and out contracts, which can be replaced with assert()s. In no way did I mean to imply that assert()s were a mistake! I've thought for 35 years that assert()s can be the input to a program prover, i.e. it's nothing new, but I do not have the expertise to figure out such proofs might work, other than simplistic cases.
You need in and out contracts for modular verification.
Nov 09
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/9/2019 4:23 AM, Timon Gehr wrote:
 You need in and out contracts for modular verification.
You can pick up both from looking at the assert's in the prolog and epilog of the function. More importantly, nobody is working on a modular verification system for D, and haven't for 20 years, so the contracts aren't particularly useful.
Nov 09
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 10.11.19 00:23, Walter Bright wrote:
 On 11/9/2019 4:23 AM, Timon Gehr wrote:
 You need in and out contracts for modular verification.
You can pick up both from looking at the assert's in the prolog and epilog of the function. ...
- Modular verification means it's enough to have DI files for functions you call, without a function body. - Some asserts in the prologue of your function might really be asserts and not assumes. - Similarly, some asserts in the epilogue of your function might not be things you actually want to guarantee to the caller.
 More importantly, nobody is working on a modular verification system for 
 D, and haven't for 20 years, so the contracts aren't particularly useful.
Programmers can read contracts too, not just verification systems. They are useful documentation and can be used for assigning blame: Is the assertion failure the fault of the caller or the callee?
Nov 10
next sibling parent Doc Andrew <x x.com> writes:
On Sunday, 10 November 2019 at 10:22:27 UTC, Timon Gehr wrote:
 - Modular verification means it's enough to have DI files for 
 functions you call, without a function body.
In a unit testing world, every assert gets checked every time the function is called anyhow, so it makes little difference whether they are pre or post-conditions, or just sprinkled throughout a function. In a verified world, it makes a _huge_ difference. A verified function with an "in" contract states, "this function satisfies all of its contracts (explicit and implicit) _if and only if_ the in contracts/preconditions are satisfied". With this, once that function is verified, a caller need only make sure that it satisfies those preconditions at each call site. In the absence of preconditions, the verifier has to re-prove _every_ assert() in the callee function (and every OTHER function that the callee uses too...) _every time_ it's called throughout the program. It's an exponential increase in the problem space. You _might_ be able to do a flow analysis to suss out which asserts are considered preconditions without explicitly stating so, but it seems like a tough problem, and explicitly stating them seems like a better practice anyhow. Modular verification is really the only tractable way to approach the problem. You build up the proof starting from leaf functions which, once proven, need only their pre-conditions checked at subsequent calls. Globals and functions with side-effects complicate this somewhat, but for pure functions it works very cleanly. And like Timon said, in the absence of in/ out contracts in a .di file, verified libraries provide no way to extend their guarantees to the user. -Doc
Nov 10
prev sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/10/2019 2:22 AM, Timon Gehr wrote:
 On 10.11.19 00:23, Walter Bright wrote:
 On 11/9/2019 4:23 AM, Timon Gehr wrote:
 You need in and out contracts for modular verification.
You can pick up both from looking at the assert's in the prolog and epilog of the function. ...
- Modular verification means it's enough to have DI files for functions you call, without a function body.
I know.
 - Some asserts in the prologue of your function might really be asserts and
not 
 assumes.
The distinction between assert and assume has come up before, and I've argued that in D they are the same.
 - Similarly, some asserts in the epilogue of your function might not be things 
 you actually want to guarantee to the caller.
You could look for this pattern: T biff(P p) { assert(something about p); T result; scope (success) assert(something about result); ... function body ... } and have the contracts.
 More importantly, nobody is working on a modular verification system for D, 
 and haven't for 20 years, so the contracts aren't particularly useful.
Programmers can read contracts too, not just verification systems. They are useful documentation and can be used for assigning blame: Is the assertion failure the fault of the caller or the callee?
I do understand the point of them. I've been enamored with contracts for 20-30 years. I've done presentations promoting them. I added them to my C++ compiler. I added them to D. I just haven't found them particularly useful or helpful when I've tried them.
Nov 11
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 11 November 2019 at 10:39:24 UTC, Walter Bright wrote:
 The distinction between assert and assume has come up before, 
 and I've argued that in D they are the same.
assert: if(failure) exit… assume: if(failure) unreachable… Can't be the same…
 I do understand the point of them. I've been enamored with 
 contracts for 20-30 years. I've done presentations promoting 
 them. I added them to my C++ compiler. I added them to D.

 I just haven't found them particularly useful or helpful when 
 I've tried them.
They are most useful when you try to learn complex third party libraries.
Nov 11
prev sibling next sibling parent Jacob Carlborg <doob me.com> writes:
On Monday, 11 November 2019 at 10:39:24 UTC, Walter Bright wrote:

 I just haven't found them particularly useful or helpful when 
 I've tried them.
There are two problems with contracts in D. 1. In-contracts are executed by the callee instead of the caller. Currently there's only a syntactic difference between an in-contract and a regular assertion inside the function body. 2. Phobos is not shipped with assertions enabled. There should be a debug version of Phobos shipped with DMD with assertions enabled. Perhaps that could be linked by default when the `-debug` flag is used. Related issues: https://issues.dlang.org/show_bug.cgi?id=6549 https://issues.dlang.org/show_bug.cgi?id=12344 https://issues.dlang.org/show_bug.cgi?id=19131 -- /Jacob Carlborg
Nov 11
prev sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 11.11.19 11:39, Walter Bright wrote:
 
 
 - Some asserts in the prologue of your function might really be 
 asserts and not assumes.
The distinction between assert and assume has come up before, and I've argued that in D they are the same.
Which I have argued is complete insanity. I'm getting pretty angry here. Not sure what to do about it.
Nov 11
parent reply Doc Andrew <x x.com> writes:
On Monday, 11 November 2019 at 22:30:18 UTC, Timon Gehr wrote:
 On 11.11.19 11:39, Walter Bright wrote:
 
 The distinction between assert and assume has come up before, 
 and I've argued that in D they are the same.
Which I have argued is complete insanity. I'm getting pretty angry here. Not sure what to do about it.
I'd expect a FV DIP to hash this out and get everybody on the same page. Different languages, different textbooks, different mathematicians all use slightly different vocabularies for this stuff, so it can get confusing. Other languages are pretty clear on the distinction between assumptions and assertions. F* ("assume" - https://www.riseforfun.com/FStar/tutorialcontent/guide#h24) & SPARK ("pragma Assume" - https://docs.adacore.com/spark2014-docs/html/ug/en/source/ass rtion_pragmas.html) both make clear that assumptions are treated like axioms in their provers, and must be used with caution. The Boogie IVL ("assume" - http://chrisposkitt.com/files/teaching/SV-2015-AutoActiveVerification.pdf) works the same way. Coq has no "assume" keyword, but the "assumption" tactic takes a hypothesis/premise and if it matches the goal (thing you're trying to prove/assert), then it solves the goal). Frama-C/ANSI C Specification Language ("assumes" clause - https://frama-c.com/download/acsl-1.14.pdf) just treats assumptions as hypotheses/premises that imply some conclusion, so pre-conditions, as far as I can tell. This might be where Walter is coming from in saying that Asserts and Assumes would be the same in D. This is the only example I could find that uses "assume" like this, but there may be others. I think _most_ people consider Assert vs Assume the way SPARK and F* do - as seen here: https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-between-assert-and-assume/ But hey, as Frama-C shows, it's not the only way to interpret those keywords. The English language gets in our way sometimes. Inflammable = flammable, and all that. If "assume" is taken to mean an "assert" which is a pre-condition, then fine, we could always point to Frama-C/ACSL to show that D isn't some insane outlier and that we aren't a bunch of backwards idiots. It wouldn't be the way _I_ would do it, but that's just one man's opinion, and I'm biased by my use of SPARK where pragma Assume has a clear meaning and works fine. Given that we already have assert() in in{} contracts, to me the assume() keyword (in Walter's reckoning of the meaning) is redundant, and could be used for the axiomatic meaning. If in{} and out{} contracts ever disappeared from the language, I think an external solver would need something like assume()/require() to distinguish preconditions from normal assertions. Having said all that, we probably need to use a little more mathematical rigor with how we define these regardless of the words we choose to describe the concepts. It would also mean we'd need another keyword/UDA to use for an axiom, like, uh, axiom. But then we're getting into weird math terms that scare people off. So that's probably why "assume" is preferred by some of the others. -Doc
Nov 11
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 12 November 2019 at 04:25:57 UTC, Doc Andrew wrote:
 so pre-conditions, as far as I can tell. This might be where 
 Walter is coming from in saying that Asserts and Assumes would 
 be the same in D. This is the only example I could find that 
 uses "assume" like this, but there may be others.
He meant that asserts are turned into assumes as an optimization. He has explained his position before in an older thread. It kinda might work in some settings if you can limit the assumed facts to a single function, but that is not how LLVM works. So it could work in dmd, but a bit dangerous. It would be a disaster in the two other D compilers. Microsoft c++ uses __assume for giving facts to the optimizer. D should stick with that,
Nov 11
prev sibling next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/11/2019 8:25 PM, Doc Andrew wrote:
 I think _most_ people consider Assert vs Assume the way SPARK and F* do - as 
 seen here: 
 https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-betwee
-assert-and-assume/ 
Which says: "Intuitively, Assert is something that you expect the static checker be able to prove at compile time, whereas Assume is something that the static checker can rely upon, but it will not try to prove. At runtime Assert and Assume behave the same: If the condition is false, then the program fails – how it fails (e.g., throwing an exception, opening a dialog box, etc. can be completely customized with CodeContracts)." Therefore after the Assert, the prover can assume the Assert condition is true. If the prover can prove the Assert is always true, the runtime check can be safely removed.
Nov 12
parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 12.11.19 10:12, Walter Bright wrote:
 On 11/11/2019 8:25 PM, Doc Andrew wrote:
 I think _most_ people consider Assert vs Assume the way SPARK and F* 
 do - as seen here: 
 https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-betwee
-assert-and-assume/ 
Which says: "Intuitively, Assert is something that you expect the static checker be able to prove at compile time, whereas Assume is something that the static checker can rely upon, but it will not try to prove.
Here, I was talking specifically using verification terminology, where the difference is obviously night and day. Then you dismissed my post by claiming in D they are the same. You might as well declare that from now on true is the same as false in D and hence you can reach any desired conclusion, but that won't change my understanding of logic, nor would I applaud your design choice.
 At runtime 
 Assert and Assume behave the same: If the condition is false, then the 
 program fails – how it fails (e.g., throwing an exception, opening a 
 dialog box, etc. can be completely customized with CodeContracts)."
 
 Therefore after the Assert, the prover can assume the Assert condition 
 is true. If the prover can prove the Assert is always true, the runtime 
 check can be safely removed.
(Technically, probably no, as last time I checked, the code contracts prover still implicitly assumed there cannot be integer overflow.) Maybe, but in D assertions get converted into optimizer assumptions in release mode _without_ any such proof being provided.
Nov 12
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/12/2019 2:26 AM, Timon Gehr wrote:
 At runtime Assert and Assume behave the same: If the condition is false, then 
 the program fails – how it fails (e.g., throwing an exception, opening a 
 dialog box, etc. can be completely customized with CodeContracts)."

 Therefore after the Assert, the prover can assume the Assert condition is 
 true. If the prover can prove the Assert is always true, the runtime check can 
 be safely removed.
(Technically, probably no, as last time I checked, the code contracts prover still implicitly assumed there cannot be integer overflow.)
D doesn't have a contracts prover, and if it did, I think it would be a mistake to ignore integer overflow. What would be of value is being able to prove integer overflow does not happen. Note that the Value Range Propagation logic in D is able to do some nice work that does take into account overflows. The global optimizer data flow analysis I wrote long ago would be broken if it didn't concern itself with overflows. In particular, loop induction variable optimization wouldn't work.
 Maybe, but in D assertions get converted into optimizer assumptions in release 
 mode _without_ any such proof being provided.
True, but D doesn't have a prover anyway :-) The user has complete control over whether asserts are checked at runtime or not. The thing about -release mode is the result of being bludgeoned in the press for having "slow" code because a competitor didn't generate the checks and the ignorant journalist did not understand this and did not ask before going to press. I last tried Spark many years ago, and discovered its contract prover was so limited I concluded it had little practical value. (If I recall, it couldn't deduce things like odd and even.) I'm sure it has improved since, but how much, I have no idea.
Nov 12
next sibling parent Timon Gehr <timon.gehr gmx.ch> writes:
On 12.11.19 12:31, Walter Bright wrote:
 On 11/12/2019 2:26 AM, Timon Gehr wrote:
 At runtime Assert and Assume behave the same: If the condition is 
 false, then the program fails – how it fails (e.g., throwing an 
 exception, opening a dialog box, etc. can be completely customized 
 with CodeContracts)."

 Therefore after the Assert, the prover can assume the Assert 
 condition is true. If the prover can prove the Assert is always true, 
 the runtime check can be safely removed.
(Technically, probably no, as last time I checked, the code contracts prover still implicitly assumed there cannot be integer overflow.)
D doesn't have a contracts prover, and if it did, I think it would be a mistake to ignore integer overflow.
(Sure. Just saying that is what their prover does, so you actually can't eliminate the check based on that.)
 What would be of value is being able 
 to prove integer overflow does not happen. Note that the Value Range 
 Propagation logic in D is able to do some nice work that does take into 
 account overflows.
 ...
(I know. I contributed some code to that.)
 The global optimizer data flow analysis I wrote long ago would be broken 
 if it didn't concern itself with overflows. In particular, loop 
 induction variable optimization wouldn't work.
 ...
It's funny you would bring that up, because it indeed does not work: https://issues.dlang.org/show_bug.cgi?id=16268
 
 Maybe, but in D assertions get converted into optimizer assumptions in 
 release mode _without_ any such proof being provided.
True, but D doesn't have a prover anyway :-) ...
Yes, it does, just not for functional correctness. D has a safe fragment where the compiler automatically proves absence of memory safety problems. asserts are allowed in safe code. Assuming incorrect propositions in your optimizer can cause memory corruption. See the problem?
 The user has complete control over whether asserts are checked at 
 runtime or not.
No. You either check, or you risk UB. Complete control looks different.
 The thing about -release mode is the result of being 
 bludgeoned in the press for having "slow" code because a competitor 
 didn't generate the checks and the ignorant journalist did not 
 understand this and did not ask before going to press.
 ...
Well, now you can be bludgeoned in the press for having "unsafe" code, because the ignorant journalist called into some library with an assertion in it. Even if they decide to ask, your response would make their article more juicy, not less.
 I last tried Spark many years ago, and discovered its contract prover 
 was so limited I concluded it had little practical value. (If I recall, 
 it couldn't deduce things like odd and even.) I'm sure it has improved 
 since, but how much, I have no idea.
 
I never tried Spark and it's entirely plausible that they were/are vastly behind the state of the art in verification research.
Nov 12
prev sibling parent reply Doc Andrew <x x.com> writes:
On Tuesday, 12 November 2019 at 11:31:43 UTC, Walter Bright wrote:
 True, but D doesn't have a prover anyway :-)
...yet :) But in one sense, we already do. The run-time behavior of disabled assertions and checks basically just assumes you've worked through a "proof" of the program using your unit-testing.
 I last tried Spark many years ago, and discovered its contract 
 prover was so limited I concluded it had little practical 
 value. (If I recall, it couldn't deduce things like odd and 
 even.) I'm sure it has improved since, but how much, I have no 
 idea.
You might be asking too much from some of the solvers. It's worth slogging through some manual proofs with a proof assistant like Coq (highly-recommended resource: https://softwarefoundations.cis.upenn.edu/). After that, what an SMT solver is able to do on it's own seems very nice :) Having said that, SPARK still requires a frustrating amount of hand-holding at times. You're able to do things like this now: ``` ------------------------------------------- -- double.ads (specification) ------------------------------------------- package double with SPARK_Mode => On is type SomeArrayType is array (Positive range <>) of Natural; function doubleArray(arr : in SomeArrayType) return SomeArrayType with Global => null, Depends => (doubleArray'Result => arr), -- set arbitrary range here in precondition to avoid overflow Pre => (for all idx in arr'Range => arr(idx) in 0..20000), -- prove that everything in the return array is even Post => (for all idx in arr'Range => isEven(doubleArray'Result(idx))); function isEven(num : in Natural) return Boolean with Contract_Cases => (num rem 2 = 0 => isEven'Result = True, num rem 2 /= 0 => isEven'Result = False); end double; ------------------------------------------- -- double.adb (implementation) ------------------------------------------- package body double is function doubleArray(arr : in SomeArrayType) return SomeArrayType with SPARK_Mode => On is doubled : SomeArrayType(arr'Range) := (others => 0); begin for i in arr'Range loop doubled(i) := 2 * arr(i); pragma Loop_Invariant(for all j in arr'First .. i => doubled(j) = 2 * arr(j)); end loop; return doubled; end doubleArray; function isEven(num : in Natural) return Boolean with SPARK_Mode => On is begin if num rem 2 = 0 then return True; else return False; end if; end isEven; end double; ------------------------------------------- -- main.adb ------------------------------------------- with Ada.Text_IO; with double; use double; procedure Main with SPARK_Mode => On is arr : SomeArrayType := (3, 7, 8, 0, 1); result : SomeArrayType := doubleArray(arr); begin for i in result'Range loop Ada.Text_IO.Put(Integer'Image(result(i)) & ", "); end loop; end Main; ``` The lame thing is the pragma Loop_Invaraiant. In order to be able to make any conclusions about the array as a whole, you've got to explain how the array looks at each point in the loop. Without that, the prover can't prove that your post-condition is true. My understanding is that SPARK needs a lot fewer of these than it used to, but it's still annoying. Still, I think it's kind of neat that you can prove that kind of behavior at compile-time, no run-time checks or unit-tests required! -Doc
Nov 12
parent Walter Bright <newshound2 digitalmars.com> writes:
On 11/12/2019 11:05 AM, Doc Andrew wrote:
 Still, I think it's kind of neat that you can prove that kind of behavior at 
 compile-time, no run-time checks or unit-tests required!
It is neat indeed.
Nov 12
prev sibling parent reply Timon Gehr <timon.gehr gmx.ch> writes:
On 12.11.19 05:25, Doc Andrew wrote:
 ...
 Other languages are pretty clear on the distinction between assumptions 
 and assertions. F* ("assume" - 
 https://www.riseforfun.com/FStar/tutorialcontent/guide#h24) & SPARK 
 ("pragma Assume" - 
 https://docs.adacore.com/spark2014-docs/html/ug/en/source/ass
rtion_pragmas.html) 
 both make clear that assumptions are treated like axioms in their 
 provers, and must be used with caution. The Boogie IVL ("assume" - 
 http://chrisposkitt.com/files/teaching/SV-2015-AutoActiveVerification.pdf) 
 works the same way.
 ...
Yup.
 Coq has no "assume" keyword, but the "assumption" tactic takes a 
 hypothesis/premise and if it matches the goal (thing you're trying to 
 prove/assert), then it solves the goal).
 ...
Sure, it is shorthand for "there is an assumption that proves the goal". This is a completely standard usage.
 Frama-C/ANSI C Specification Language ("assumes" clause - 
 https://frama-c.com/download/acsl-1.14.pdf) just treats assumptions as 
 hypotheses/premises that imply some conclusion, so pre-conditions, as 
 far as I can tell. This might be where Walter is coming from in saying 
 that Asserts and Assumes would be the same in D.
It is not. Walter is arguing about run-time semantics and he uses some weird argument ("-release only removes the check, it doesn't remove the assumption") to justify the unsafe behavior of asserts with -release.
 This is the only 
 example I could find that uses "assume" like this, but there may be others.
 ...
The 'assumes' clause just says what assumptions are that the _function_ makes in order to satisfy the postcondition. It's saying "this function assumes ...", not "verifier, please assume ...". This is how preconditions operate. The function indeed assumes something, but it puts a burden on a caller who may not want to assume it.
 I think _most_ people consider Assert vs Assume the way SPARK and F* do 
 - as seen here: 
 https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-betwee
-assert-and-assume/ 
 
 
 But hey, as Frama-C shows, it's not the only way to interpret those 
 keywords.
Frama-C shows no such thing. I'm not confused at all by an 'assumes' clause in a function signature that signifies a precondition.
 The English language gets in our way sometimes. Inflammable = 
 flammable, and all that.
 
 If "assume" is taken to mean an "assert" which is a pre-condition,
Just to be clear: I have no problem at all with D's usage of 'assert' in preconditions. My point was that if you get rid of preconditions, 'assert' cannot express preconditions, so the prover won't know whether the callee or the caller is responsible for discharging a certain assertion.
 then 
 fine, we could always point to Frama-C/ACSL to show that D isn't some 
 insane outlier and that we aren't a bunch of backwards idiots.
The -release flag turns asserts into optimizer assumptions. In -release mode, a failing assertion in safe code is undefined behavior. (In the C sense.) Assume cannot be safe, while assert can, but Walter conflates them into the same construct.
 It 
 wouldn't be the way _I_ would do it, but that's just one man's opinion, 
 and I'm biased by my use of SPARK where pragma Assume has a clear 
 meaning and works fine.
 
 Given that we already have assert() in in{} contracts, to me the 
 assume() keyword (in Walter's reckoning of the meaning) is redundant, 
 and could be used for the axiomatic meaning.
 ...
Given that we have 'in' contracts, but we were arguing specifically about a scenario where we don't have them.
 If in{} and out{} contracts ever disappeared from the language, I think 
 an external solver would need something like assume()/require() to 
 distinguish preconditions from normal assertions.
 ...
Yes, this was exactly my point.
Nov 12
parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 11/12/2019 2:51 AM, Timon Gehr wrote:
 If in{} and out{} contracts ever disappeared from the language, I think an 
 external solver would need something like assume()/require() to distinguish 
 preconditions from normal assertions.
 ...
Yes, this was exactly my point.
The precondition would just be the sequence of assert()s before any other code, and the postcondition is the sequence that appears after any other code. It's not a challenge to pull that out of the AST.
Nov 12
parent Timon Gehr <timon.gehr gmx.ch> writes:
On 12.11.19 12:35, Walter Bright wrote:
 On 11/12/2019 2:51 AM, Timon Gehr wrote:
 If in{} and out{} contracts ever disappeared from the language, I 
 think an external solver would need something like assume()/require() 
 to distinguish preconditions from normal assertions.
 ...
Yes, this was exactly my point.
The precondition would just be the sequence of assert()s before any other code, and the postcondition is the sequence that appears after any other code.
I understand, and this strategy has the weaknesses I pointed out.
 It's not a challenge to pull that out of the AST.
Of course it is not challenging to implement. The point is that it is not a great idea, not that it is hard to do.
Nov 12
prev sibling parent Paolo Invernizzi <paolo.invernizzi gmail.com> writes:
On Friday, 8 November 2019 at 03:43:56 UTC, Walter Bright wrote:
 On 11/7/2019 7:34 AM, Paolo Invernizzi wrote:
 On Thursday, 7 November 2019 at 09:41:05 UTC, Timon Gehr wrote:
 On 07.11.19 08:34, drug wrote:
 On 11/7/19 3:00 AM, Walter Bright wrote:
 Not that this is necessarily a bad thing, as I also promote 
 the safe/unsafe code dichotomy.
And I'm totally agree to you. That's the good engineering approach. But the Rust community is overselling Rust safety and this confuses me at least.
http://plv.mpi-sws.org/rustbelt/
"... Any realistic languages targeting this domain in the future will encounter the same problem ..." I underline _realistic_  ... Sorry Walter, I'm all with Timon on that.
I don't see anything on that site that contradicts what I wrote. In particular: "Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary. The hope is that such "unsafe" code is properly encapsulated, so that Rust's language-level safety guarantees are preserved. But due to Rust's reliance on a weak memory model of concurrency, along with its bleeding-edge type system, verifying that Rust and its libraries are actually safe will require fundamental advances to the state of the art." is saying the same thing.
Agreed, and I definitely appreciate your effort in pushing towards mechanic verification on that topic. What I mean is that there will be the need for manual verification also, when libraries will be forced to rely on unsafe code. To my understanding, the project is providing guidance in doing that (manual) verification of unsafe code. My advice is to work tightly coupled with Timon, to have a clear understanding of what is theoretically feasible and what not, for mechanical check, and to try to have clear borders around the two arenas. In that way, you can concentrate on implementing and polishing what is pragmatically doable in the compiler, in a mechanical way, avoiding efforts towards dead ends. But hey, you have already surprised us all when you designed D ... I will be glad to see that your idea really works! /Paolo
Nov 08
prev sibling parent =?UTF-8?Q?Ali_=c3=87ehreli?= <acehreli yahoo.com> writes:
On 11/07/2019 07:34 AM, Paolo Invernizzi wrote:

 http://plv.mpi-sws.org/rustbelt/
"... Any realistic languages
On a lighter note, that's an uncharacteristically nonacademic phrase.
  targeting this domain in the future
Is that an example of common ignorance towards D or do they accept D as being already safe, or perhaps the future is already here with D? :) On a more serious note, I very much appreciate Rust, their taking D seriously, and any work towards software safety. Ali
Nov 08
prev sibling parent reply jmh530 <john.michael.hall gmail.com> writes:
On Thursday, 7 November 2019 at 00:00:28 UTC, Walter Bright wrote:
 

 D needs to make  safe the default, though.
In terms of a timeline, can I assume that there are no plans for this until a D 3.0?
Nov 07
parent reply Mike Parker <aldacron gmail.com> writes:
On Thursday, 7 November 2019 at 11:33:35 UTC, jmh530 wrote:
 On Thursday, 7 November 2019 at 00:00:28 UTC, Walter Bright 
 wrote:
 

 D needs to make  safe the default, though.
In terms of a timeline, can I assume that there are no plans for this until a D 3.0?
https://github.com/dlang/DIPs/pull/166
Nov 07
parent jmh530 <john.michael.hall gmail.com> writes:
On Thursday, 7 November 2019 at 12:06:07 UTC, Mike Parker wrote:
 [snip]
 In terms of a timeline, can I assume that there are no plans 
 for this until a D 3.0?
https://github.com/dlang/DIPs/pull/166
Ah, I hadn't realized a DIP was in the works. Given that it is a Walter DIP, that means it has a high likelihood of being accepted...
Nov 07
prev sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Wednesday, 6 November 2019 at 05:02:10 UTC, Walter Bright 
wrote:
 I'm going to speculate that Rust is a bit like pure functional 
 programming. It's a great paradigm, but is inconvenient for 
 that last mile of the code one needs to write.
Yes, but I guess one could say that for Go as well. On the other hand, the number of projects in Go seems to taper off, while the number of contributors is steadily increasing. So in the case of Go that might suggest that people are now able to find libraries that are suitable and start contributing to those instead of creating new ones. So, Go appears to have found a stable niche where it can become solid. Despite being inconvenient in some ways, and quite frankly, despite missing features that is welcome when writing larger programs. In the case of Rust, it is expanding, and it seems like people are in the process of figuring out how to best write libraries for it and to figure out where Rust is the best solution. I would expect Rust to do really well in all larger server scenarios in the long term, where you often deal with many objects, tree-like structures, require reliability and also need memory-efficiency. I would expect Rust to do less well in audio/video/embedded, unless some really good Rust-frameworks appear that let you do audio/video/embedded in a high level fashion. Which could happen, e.g. if the Firefox team invest in reusable audio/video components for Rust. Swift isn't really a great language for audio/video either (for other reasons), but it works out because of the frameworks Apple provide as a foundation. I don't see anything in the Rust semantics that prevents it from becoming a good semi-high-level language for writing applications and servers. It all hangs on whether it eventually provides a good multi-platform framework.
 This is why D has "pure" functions. You can slip in and out of 
 functional programming as you like.

 I'm working on an ownership/borrowing system for D. But the 
 idea is it will only be active in functions marked as  live.
The trend is going towards programmers expecting to spend less effort on speccing function signatures and have the IDE/compiler du more of that by static analysis, flow-typing and the like. That is an argument against Rust, but also against attributes...
Nov 06
prev sibling parent Guillaume Piolat <first.last gmail.com> writes:
On Monday, 4 November 2019 at 09:32:56 UTC, NaN wrote:
 You'd think with all the press rust seems to be getting lately 
 it'd be higher up than it is?
It is also surprising to me, but I was said TIOBE is based on job offers. Other indexes are often based on Github and StackOverflow presence, which ultimately depend on how online/hobbyist the community is. Popular languages are ranked differently depending on whether you measure "dark matter" developers that don't interact online, or users of more social websites like Github and StackOverflow that will be biased towards talkative people.
Nov 04
prev sibling next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 4 November 2019 at 09:03:04 UTC, RazvanN wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming languages 
 [1], landing on the 18th position. I have been keeping an eye 
 on this index, and it is for the first time that I see this 
 happening.
It favours older languages that are present on many websites. Tiobe measures the number of hits for the search "d programming" and "dlang programming". However, for D there are false positives, so they assume 90% confidence... Although they also remove "3-D programming" and "Dtrace". Anyway, this is not a good metric. It is strongly affected by search engine ranking strategies and online structure. (many small sites vs one big site, etc). Ola.
Nov 04
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 4 November 2019 at 21:09:47 UTC, Ola Fosheim Grøstad 
wrote:
 programming" and "dlang programming". However, for D there are 
 false positives, so they assume 90% confidence... Although they
FWIW, you'll see hits on things like: a) … b) … c) … d) programming is a… Or stuff like: …ph.d. programming… But they only look at the relevance for the first 100 hits when estimating the confidence metric, which isn't really compatible with how you can structure ranking in a search engine. You might get less confidence the further down the ranking list you get. E.g the first 100 could give 100% confidence, but then as the ranker is running out of "good matches" the number of false positives could increase significantly... Also... the search engine might do a cut-off or use a predetermined hit-list for popular searches... Too many potential sources for significant bias in Tiobe (and aggregating results from many search engines does not make that better, could even make it worse).
Nov 04
prev sibling next sibling parent Walter Bright <newshound2 digitalmars.com> writes:
On 11/4/2019 1:03 AM, RazvanN wrote:
 Good news, everyone!
 
 D has entered the Tiobe top 20 ranking of programming languages [1], landing
on 
 the 18th position. I have been keeping an eye on this index, and it is for the 
 first time that I see this happening.
 
 Cheers,
 RazvanN
 
 [1] https://www.tiobe.com/tiobe-index/
 
 
Great news! (It's been there before, until Tiobe changed their ranking method.)
Nov 04
prev sibling next sibling parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Monday, 4 November 2019 at 09:03:04 UTC, RazvanN wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming languages 
 [1], landing on the 18th position. I have been keeping an eye 
 on this index, and it is for the first time that I see this 
 happening.

 Cheers,
 RazvanN

 [1] https://www.tiobe.com/tiobe-index/
I've been keeping an eye on the Tiobe index in the last couple of months and I started to notice that D had a slow but steady upwards trend. It was in the 22. and 21. place in the last two months. I'm a bit surprised that it jumped all the way to 18. place. It's a good thing that this happened because the index has a lot of visibility. Journalists like to write a lot about it for some reason. However, this index is quite noisy and flawed in several ways. So this high rating for D might be a fluke and next month D might be back to 21. place... I'm really hoping that D is starting to show up in the top 20 more often than not in the coming months. If you take other indices like the more complex Redmonk index that takes its data from Stackoverflow and Github and is thus biased towards open source projects, you get totally different results. For example, the Redmonk index ranks rust pretty high. This shows how arbitrary these rankings are in the end.
Nov 04
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 5 November 2019 at 02:08:28 UTC, Gregor Mückl wrote:
 However, this index is quite noisy and flawed in several ways.
Right, the big dips in the graph are from Google adjusting their ranker... AFAIK.
Nov 05
prev sibling next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 5 November 2019 at 02:08:28 UTC, Gregor Mückl wrote:
 If you take other indices like the more complex Redmonk index 
 that takes its data from Stackoverflow and Github and is thus 
 biased towards open source projects, you get totally different 
 results. For example, the Redmonk index ranks rust pretty high. 
 This shows how arbitrary these rankings are in the end.
Redmonk is flawed as well, of course. A language with worse documentation, is more difficult to use or appeal more to beginners (like PhP) will have a stronger presence on Stackoverflow... Github is probably the better metric, but counting number of projects is silly. Some languages have a culture of miniature repositories. Others have lots of forking. But yeah, if you did static analysis on all the source code on Github then that could measure something reasonable. Also the counting on Github seems to be approximate. I get ±10% in repeated searches their web interface, e.g. sometimes 7000 hits, sometimes 8000 hits… Searches on github: 2k language:nim 8k language:d 10k language:julia 23k language:go 43k language:rust 759k language:c 880k language:c# 890k language:c++ 3400k language:java
Nov 05
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
Ok, so here is another github metric that is more interesting. 
Doing a "language:d" search and then look at the number of 
_users_:

Zig: 10
Pony: 25
Nim:  400
Crystal: 500
Ada:  600
Vala: 800
D:     2000
Pascal: 12000
Dart: 13000
Rust: 16000
Swift: 24000
Go:   128000
C++: 706000

Clearly, this metric favours older languages. It would have been 
better to look at new repos only, but I don't know if that is 
possible with the github interface.
Nov 05
next sibling parent reply Daniel Kozak <kozzi11 gmail.com> writes:
On Tue, Nov 5, 2019 at 11:50 AM Ola Fosheim Grøstad via Digitalmars-d
<digitalmars-d puremagic.com> wrote:

I am using openhub interface:

https://www.openhub.net/languages/compare?utf8=✓&measure=commits&language_name%5B%5D=erlang&language_name%5B%5D=dmd&language_name%5B%5D=-1&language_name%5B%5D=-1&language_name%5B%5D=-1&commit=Update
Nov 05
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 5 November 2019 at 11:45:59 UTC, Daniel Kozak wrote:
 I am using openhub interface:
Thanks, it seems to be buggy tough: https://www.openhub.net/languages/compare?utf8=%E2%9C%93&measure=contributors&language_name%5B%5D=dmd&language_name%5B%5D=golang&language_name%5B%5D=rust&language_name%5B%5D=cpp&language_name%5B%5D=-1&commit=Update Sharp dip for Go, and sharp peak for C++? ("Nim" does not seem to be present as an option.)
Nov 05
next sibling parent Daniel Kozak <kozzi11 gmail.com> writes:
On Tue, Nov 5, 2019 at 1:05 PM Ola Fosheim Grøstad via Digitalmars-d
<digitalmars-d puremagic.com> wrote:
 On Tuesday, 5 November 2019 at 11:45:59 UTC, Daniel Kozak wrote:
 I am using openhub interface:
Thanks, it seems to be buggy tough: https://www.openhub.net/languages/compare?utf8=%E2%9C%93&measure=contributors&language_name%5B%5D=dmd&language_name%5B%5D=golang&language_name%5B%5D=rust&language_name%5B%5D=cpp&language_name%5B%5D=-1&commit=Update Sharp dip for Go, and sharp peak for C++? ("Nim" does not seem to be present as an option.)
Yes, this is common issue there, but if you look at it nex month it would be ok, I am not sure why this happening.
Nov 05
prev sibling next sibling parent reply Daniel Kozak <kozzi11 gmail.com> writes:
On Tue, Nov 5, 2019 at 1:24 PM Daniel Kozak <kozzi11 gmail.com> wrote:
 On Tue, Nov 5, 2019 at 1:05 PM Ola Fosheim Grøstad via Digitalmars-d
 <digitalmars-d puremagic.com> wrote:
 On Tuesday, 5 November 2019 at 11:45:59 UTC, Daniel Kozak wrote:
 I am using openhub interface:
Thanks, it seems to be buggy tough: https://www.openhub.net/languages/compare?utf8=%E2%9C%93&measure=contributors&language_name%5B%5D=dmd&language_name%5B%5D=golang&language_name%5B%5D=rust&language_name%5B%5D=cpp&language_name%5B%5D=-1&commit=Update Sharp dip for Go, and sharp peak for C++? ("Nim" does not seem to be present as an option.)
Yes, this is common issue there, but if you look at it nex month it would be ok, I am not sure why this happening.
OK I guess the issue is with not all current data are process yet. So they have statistic for D, for C++ but not for Go, so because it is in percent and there are data only fo few languages it would seems like there are peeks and dips
Nov 05
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 5 November 2019 at 12:27:48 UTC, Daniel Kozak wrote:
 OK I guess the issue is with not all current data are process 
 yet. So they have statistic for D, for C++ but not for Go, so 
 because it is in percent and there are data only fo few 
 languages it would seems like there are peeks and dips
Alright! It is an interesting graphing tool, for sure. I didn't find "Swift" in the menu either, btw.
Nov 05
prev sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 5 November 2019 at 12:04:25 UTC, Ola Fosheim Grøstad 
wrote:
 On Tuesday, 5 November 2019 at 11:45:59 UTC, Daniel Kozak wrote:
 I am using openhub interface:
Thanks, it seems to be buggy tough:
Ok, so OpenHub is flawed for 2019, but from 2016-2019 we can see that for Ada, Vala, HaXe and D there has been stagnation. For Pascal there has been a decline and for OCaml growth: https://www.openhub.net/languages/compare?utf8=%E2%9C%93&measure=contributors&language_name%5B%5D=ada&language_name%5B%5D=crystal&language_name%5B%5D=dmd&language_name%5B%5D=-1&language_name%5B%5D=ocaml&language_name%5B%5D=pascal&language_name%5B%5D=vala&language_name%5B%5D=-1&commit=Update We can also see that Go and Rust have linear growth (relative), and C# is experiencing stagnation: https://www.openhub.net/languages/compare?utf8=%E2%9C%93&measure=contributors&language_name%5B%5D=csharp&language_name%5B%5D=dmd&language_name%5B%5D=golang&language_name%5B%5D=-1&language_name%5B%5D=rust&language_name%5B%5D=-1&commit=Update Also Kotlin's growth is cutting into Java, while Scala experience stagnation, but Java is still massive: https://www.openhub.net/languages/compare?utf8=%E2%9C%93&measure=contributors&language_name%5B%5D=java&language_name%5B%5D=kotlin&language_name%5B%5D=scala&language_name%5B%5D=-1&language_name%5B%5D=-1&commit=Update Nothing too surprising, I guess.
Nov 05
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 5 November 2019 at 12:35:11 UTC, Ola Fosheim Grøstad 
wrote:
 Nothing too surprising, I guess.
I guess C++/ C is worth noticing as well: https://www.openhub.net/languages/compare?utf8=%E2%9C%93&measure=contributors&language_name%5B%5D=cpp&language_name%5B%5D=c&language_name%5B%5D=-1&commit=Update So C is experiencing stagnation, but C++ apparently has linear growth from C++14 onwards. 10% of all contributors on Github committing C++ code seems a bit too much. Probably some overcounting, people who commit non-C++ code to a mixed language project will count as a C++ contributor on Open Hub. Maybe more multi-language-projects have started to use C++ for low level libraries? Dunno, but regardless, continuous language improvements seem to pay off in terms of increased adoption.
Nov 05
prev sibling next sibling parent reply user5678 <user5678 1234.de> writes:
On Tuesday, 5 November 2019 at 10:49:43 UTC, Ola Fosheim Grøstad 
wrote:
 Ok, so here is another github metric that is more interesting. 
 Doing a "language:d" search and then look at the number of
This GH feature doesn't work well IMO. I had an account with several D language projects and once I read all the results (someting like 100 pages !) and wasn't listed.
Nov 05
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 5 November 2019 at 19:12:31 UTC, user5678 wrote:
 This GH feature doesn't work well IMO. I had an account with 
 several D language projects and once I read all the results 
 (someting like 100 pages !) and wasn't listed.
:-/ Hopefully all languages are affected in the same way...
Nov 05
prev sibling parent reply GoaLitiuM <goalitium dforums.mail.kapsi.fi> writes:
On Tuesday, 5 November 2019 at 10:49:43 UTC, Ola Fosheim Grøstad 
wrote:
 Ok, so here is another github metric that is more interesting. 
 Doing a "language:d" search and then look at the number of 
 _users_
How does this even work? I tried this and added myself to the search and couldn't find me listed there despite working in multiple D related repos both mine and others. It does list all my PRs and commits but not me as an user.
Nov 06
next sibling parent user5678 <user5678 1234.de> writes:
On Wednesday, 6 November 2019 at 15:40:11 UTC, GoaLitiuM wrote:
 On Tuesday, 5 November 2019 at 10:49:43 UTC, Ola Fosheim 
 Grøstad wrote:
 Ok, so here is another github metric that is more interesting. 
 Doing a "language:d" search and then look at the number of 
 _users_
How does this even work? I tried this and added myself to the search and couldn't find me listed there despite working in multiple D related repos both mine and others. It does list all my PRs and commits but not me as an user.
I suspect that mentioning dlang in your public bio is a factor of inclusion
Nov 06
prev sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Wednesday, 6 November 2019 at 15:40:11 UTC, GoaLitiuM wrote:
 How does this even work? I tried this and added myself to the 
 search and couldn't find me listed there despite working in 
 multiple D related repos both mine and others. It does list all 
 my PRs and commits but not me as an user.
Good question, Github is rather mysterious entity sometimes… I think the above mentioned Open Hub is a much better resource for measuring the "social evolution" of programming languages.
Nov 06
prev sibling parent Walter Bright <newshound2 digitalmars.com> writes:
On 11/4/2019 6:08 PM, Gregor Mückl wrote:
 However, this index is quite noisy and flawed in several ways. So this high 
 rating for D  might be a fluke and next month D might be back to 21. place... 
 I'm really hoping that D is starting to show up in the top 20 more often than 
 not in the coming months.
The great advantage D has is our dogged persistence.
Nov 05
prev sibling next sibling parent reply Mark Rousell <mark.rousell signal100.com> writes:
On 04/11/2019 09:03, RazvanN via Digitalmars-d wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming languages [1],
 landing on the 18th position. I have been keeping an eye on this
 index, and it is for the first time that I see this happening.
Not that I am advocating gaming the Tiobe ranking protocol but I note that "ratings are based on the number of skilled engineers world-wide, courses and third party vendors. Popular search engines such as Google, Bing, Yahoo!, Wikipedia, Amazon, YouTube and Baidu are used to calculate the ratings." The above being so, a quick win for a language that wished to raise its Tiobe ranking and thus its general profile would be for its community to post lots of "course" (i.e. tutorial) videos on YouTube. It is possible that a series of videos, constituting a course, might be better still. This would potentially increase the ranking directly based upon YouTube hits. If language community blogs and forums could then link to these YouTube courses then this would, in turn, increase the language's ranking on Google, Bing, and so on. Wikipedia articles linking to the YouTube courses would also be beneficial. Just a thought. It is ironic that an increased Tiobe ranking (amongst others) can, in and of itself, increase the genuine user base of a language. (As, perhaps, with the community hype around Rust). -- Mark Rousell
Nov 04
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Tuesday, 5 November 2019 at 04:00:02 UTC, Mark Rousell wrote:
 The above being so, a quick win for a language that wished to 
 raise its Tiobe ranking and thus its general profile would be 
 for its community to post lots of "course" (i.e. tutorial) 
 videos on YouTube.
That depends on the ranker. Seems like Google is trying to reduce the number of hits from the same website. So, with that in mind you would be better off getting bloggers on various blogging sites to write about it in different languages. See: https://www.tiobe.com/tiobe-index/programming-languages-definition/ If you look at the description of Tiobe it seems like they aggregate Google hits from various languages. So the best strategy seems to be to game Google's ranker and do it in all the languages Tiobe are tracking: Google.com: 7.69% Google.com.hk: 5.85% Google.co.in: 5.23% Google.co.jp: 4.00% Google.com.br: 3.69% Google.de: 3.38% Google.ru: 2.77% Google.fr: 2.15% Google.it: 1.85% Google.es: 1.54% Google.cn: 1.23% Google.com.tw: 0.92% Google.com.mx: 0.31%
Nov 05
prev sibling parent reply user5678 <user5678 1234.de> writes:
On Monday, 4 November 2019 at 09:03:04 UTC, RazvanN wrote:
 Good news, everyone!

 D has entered the Tiobe top 20 ranking of programming languages 
 [1], landing on the 18th position. I have been keeping an eye 
 on this index, and it is for the first time that I see this 
 happening.

 Cheers,
 RazvanN

 [1] https://www.tiobe.com/tiobe-index/
Tiobe... a great indication of how biased we are. When the language they like progress people forget that they've said about 1 million times that the Tiobe index is BS.
Nov 05
parent drug <drug2004 bk.ru> writes:
On 11/5/19 10:00 PM, user5678 wrote:
 Tiobe... a great indication of how biased we are. When the language they 
 like progress people forget that they've said about 1 million times that 
 the Tiobe index is BS.
I wouldn't say that D community is biased but in general I agree to you.
Nov 06