1. 3

    This paper is starting to gain traction and the discussion needs to broaden out; mathematics suffers from the same problems as software development

    1. 1

      That On Proof and Progress paper was great! Appreciate you sharing it. There was quite a bit of overlap between what he said and another I was reading on fixing math education. Schools focus on equations and publishing too much when real math research is more about understanding and communicating with each other. That one indicates, though, that there’s significant, avoidable problems in traditional math on communicating as well.

    1. 5

      Another paper to add to the list of claimed proofs of the N vs. NP problem:


      1. 3

        This paper is somewhat jumbled. The short version is that a a bunch of tools were run through the benchmark used for a 2017 software verification competition, where lots of systems were compared. The benchmarks were mostly short, i.e., under 20 lines, but there are lots of them.

        The programs used to represent testing were: AFL-fuzz, CPATiger, Crest-ppc, FShell, Klee, and PRtest. A somewhat odd selection to label ‘testing’, but if you are looking for automated tools, what else is there?

        The model checkers were: Cbmc, CPA-Seq, Esbmc-incr, and Esbmc-kInd.

        Figure 6 shows the ‘testing’ tools to be a lot slower than the model based tools. Is this because the testing tools are designed to work on programs that are much larger than 20 lines and so have a higher startup cost? Model based tools would certainly have performance issues with larger programs.

        Perhaps when the authors have had time to think about their results, they will write a more interesting paper (assuming the data contains something interesting).

        1. 3

          I also think they have focused entirely on the wrong benchmark.

          I really don’t care about two orders of magnitude difference in CPU time for this class of task.

          I really really do care about how much of my time and brain power is required to set up and run these tools.

          They can then run all week for all I care.

          I suspect under that benchmark, and given their results, AFL looks very very good. (And from what I have read, and from a couple of personal experiments I have run, AFL is indeed very very Good)

          Also very interesting, and I didn’t spot (on admittedly on a fast read) any deeper analysis of the factoid that fuzzers found some bugs model checkers didn’t and vice versa.

          1. 1

            They needed a benchmark that the model based tools had a chance of being able to handle; the one thy used is it.

            Me thinks the authors saw the opportunity to get a paper involving formal methods published, with their names on, that did not involve too much effort.

          2. 1

            Appreciate you taking time to enumerate weaknesses. Being able to check small modules is fine for my purposes since I advocate using methods for safe interfacing of components. However, for use with legacy software or not designed with verification, that would be a big problem for the model-checkers.

          1. 4

            A solid list, with one question mark.

            Lynn Conway started life as a man. does this mean he/then her achievements give equally credited to men/women?

            1. 52

              No. Trans women are women.

              1. 10

                Thank you . I want to live in a world where this is just taken as a given. Lets start with our little world here people.

                1. 8

                  What is the goal of creating a list of women in CS? If it’s to demonstrate to young girls that they can enter the field, it seems unproductive to include someone who grew up experiencing life as a man.

                  If the goal of creating the list is some kind of contest, then it’s counterproductive for entirely different reasons.

                  1. 28

                    someone who grew up experiencing life as a man

                    Do you know any trans women who have said they grew up experiencing life as a man? I know quite a few and none of them have expressed anything like this, and my own experience was certainly not like that.

                    However, if you mean that we were treated like men, with the privilege it brings in many areas, then yes, that became even more obvious to me the moment I came out.

                    Regardless, trans folks need role models too, and we don’t get a lot of respectful representation.

                    1. 21
                      $ curl https://www.hillelwayne.com/post/important-women-in-cs/ | grep girl | wc -l

                      The motivation for the post are clearly layed out in the first paragraph:

                      I’m tired of hearing about Grace Hopper, Margaret Hamilton, and Ada Lovelace. Can’t we think of someone else for once?

                      It’s a pretty pure writeup for the sake of being a list you can refer to.

                      On your statement about “girls”. It’s quite bad to assume a list of women is just for kids, it’s also bad to assume trans women can’t be examples to (possibly themselves trans) girls.

                      1. 4

                        That’s not a motivation, that’s a tagline.

                        The primary reason I would refer to a list like this is if I was demonstrating to a young woman considering CS that, perhaps despite appearances, many women have historically made major contributions to the field. I’m not sure what else I would need something like this for.

                        1. 5

                          Maybe its not for you to distribute but for women to discover …

                        2. 1

                          I don’t see why it’s bad to assume that. It feels like it would be a pretty serious turn off to me if I we’re looking for successful women and found people who were men into adulthood. I find it hard to imagine that I’m unique in that feeling. I’m sure it feels good for trans people but I’d that’s your goal admit the trade-off rather than just telling people they’re women and not transwomen.

                          You can berate people for not considering trans-women to be the same as born women but it will likely just keep them quiet rather than convince them to be inspired.

                          1. 19

                            people who were men into adulthood

                            Now I’m curious what your criteria are, if not self-identification. When did this person cease to be a man, to you?

                            When they changed their name?

                            When they changed their legal gender?

                            When they started hormones?

                            When they changed their presentation?

                            When they got surgery?

                            What about trans people who do none of that? E.g. I’ve changed my name and legal gender (only because governments insist on putting it in passports and whatnot,) because I had the means to do so and it bothered me enough that I did, is that enough? What about trans people who don’t have the means, option, or desire to do so?

                            When biologist say that there’s not one parameter that overrides the others when it comes to determining sex¹, and that it makes more sense to just go by a person’s gender identity if you for whatever reason must label them as male/female, why is that same gender identity not enough to determine someone’s own gender?

                            1. http://www.nature.com/news/sex-redefined-1.16943
                        3. 16

                          If it’s to demonstrate to young girls that they can enter the field, it seems unproductive to include someone who grew up experiencing life as a man.

                          This is a misunderstanding of transexuality. She grew up experiencing life as a woman, but also as a woman housed in a foreign-feeling body and facing a tendency by others to mistake her gender.

                          Does that mean she faced a different childhood from many other women? Sure. But she also shared many of the disadvantages they faced, frequently to a much stronger degree. Women face difficulty if they present as “femme” in this field, but it is much more intense if they present as femme AND people mis-bucket them into the “male” mental box.

                      2. 14

                        If they identified as a woman at the time of accomplishment, it seems quite reasonable that it’d count. For future work, just think about it in terms of trans-woman extends base class woman or at least implements the woman interface.

                        In any event, your comment is quite off-topic. Rehashing this sort of stuff is an exercise that while interesting is better kept literally anywhere else on the internet–if you have questions of this variety, please seek enlightenment via private message with somebody you think may be helpful on the matter, and don’t derail here.

                        1. 7

                          The point of this is not to give more achievements to women… It’s to showcase people who were most likely marginalized.

                          1. [Comment removed by author]

                            1. 9

                              This is definitely not what life is like for trans people pre-transition.

                          2. 12

                            It’s rude to talk about people’s gender like this fyi

                            1. 0

                              It’s ridiculous to allow this framing to suppress a reasonable point.

                              1. 10

                                It’s not a reasonable point. This is not the place to make whatever point you’re trying to make.

                            2. 3

                              Depends on where a person is on political spectrum. I’d probably note they’re trans if targeting a wide audience, not if a liberal one, and leave person off if a right-leaning one.

                              1. 5

                                what they dont know wont hurt them. As far as the right is concerned , she is a woman …

                              2. 2

                                It is irrelevant, and you asking this is offensive.

                                1. -1

                                  Interesting question. I think it may be met with hostility, as it brings to mind the contradiction inherent in both claiming that sex/gender is arbitrary or constructed and also intentionally emphasizing the achievements of one gender. Based on the subset of my social circle that engages in this kind of thing, these activities are usually highly correlated. Picking one or the other seems to get people labeled as, respectively, some slang variation of “nerd”, or a “TERF”.

                                  1. 34

                                    Can we please not for once? Every time anything similar to this comes up the thread turns into a pissfight over Gender Studies 101. Let’s just celebrate Conway’s contributions and not get into an argument about whether she “counts”.

                                    1. 10

                                      Much as I sympathize, transgender is controversial enough that merely putting a trans person on a list that claims all its members are a specific gender will generate reactions like that due to a huge chunk of the population not recognizing the gender claim. That will always happen unless the audience totally agrees. So, one will always have to choose between not mentioning them to avoid noise or including them combating noise.

                                      1. 20

                                        I would like to live in a world where trangender isnt controversial and we dont have to waste energy discussing this. Can lobsters be that world please ?

                                        1. 18

                                          Perhaps this is why we get accused of pushing some kind of agenda or bringing politics into things, by merely existing/being visible around people who find us ”controversial” or start questioning whether our gender is legit or what have you. I usually stay out of such discussions, but sometimes feel the need to respond to claims about trans folks that I feel come from a place of ignorance rather than bigotry or malice, but most of the time I’m proven wrong and they aren’t really interested in the science or whatever they claim, they just want an excuse to say hateful things about us. I’ve had a better than average experience on this website, when it comes to responses.

                                          1. 6

                                            I cant speak for everyone on the side that denies trans identity. Just my group I guess. For us and partly for others, the root of the problem is there is a status quo with massive evidence and inertia about how we categorize gender that a small segment are countering in a more subjective way. We dont think the counters carry the weight of status quo. We also prefer objective criteria about anything involving biology or human categorization where possible. I know you’ve heard the details so I spare you that

                                            That means there will be people objecting every time a case comes up. If it seems mean, remember that there’s leftists who will be quick to counter anything they think shouldn’t be tolerated on a forum (eg language policing) on their principles. For me, Im just courteous with the pronouns and such since it has no real effect on me in most circumstances: I can default on kindness until forced to be more specific by a question or debate happening. Trans people are still people to me. So, I avoid bringing this stuff up much as possible.

                                            The dont-rock-the-boat, kinder approach wouldve been for person rejecting the gender claim to just ignore talking about the person he or she didnt think was a woman to focus on others. The thread wouldve stayed on topic. Positive things would be said about about deserving people. And so on. Someone had to stir shit up, though. (Sighs)

                                            And I agree Lobsters have handled these things much better than other places. I usually like this community even on the days it’s irritating. Relatively at least. ;)

                                            1. 6

                                              For us and partly for others, the root of the problem is there is a status quo with massive evidence and inertia about how we categorize gender that a small segment are countering in a more subjective way.

                                              I know you’re a cool dude and would be more than happy to discuss this with you in private, but I think we all mostly agree that this is now pretty outside the realm of tech, so continuing to discuss it publicly would be getting off topic :) I’ll DM you?

                                              1. 7

                                                I was just answering a question at this point as I had nothing else to say. Personally, Id rather the political topics stay off Lobsters as I voted in community guidelines thread. This tangent couldnt end sooner given how off topic and conflict-creating it is.

                                                Here’s something for you to try I did earlier. Just click the minus next to Derek’s comment. This whole thread instantly looks the way it should have in first place. :)

                                              2. 4

                                                I find the idea that everyone who disagrees with these things should avoid rocking the boat extremely disconcerting. It feels like a duty to rock it on behalf of those who agree but are too polite or afraid for their jobs or reputations to state their actual opinions, to normalize speaking honestly about uncomfortable topics.

                                                I mean, I also think it’s on topic to debate the political point made by the list.

                                                1. 4

                                                  I agree with those points. It’s why I’m in the sub-thread. The disagreement is a practical one a few others are noting:

                                                  “I mean, I also think it’s on topic to debate the political point made by the list.”

                                                  I agree. I told someone that in private plus said it here in this thread. Whether we want to bring it up, though, should depend on what the goal is. My goal is the site stays focused on interesting, preferably-deep topics with pleasant experience with minimal noise. There’s political debates and flamewars available all over the Internet with the experience that’s typical of Lobsters being a rarity. So, I’d just have not brought it up here.

                                                  When someone did, the early response was a mix of people saying it’s off-topic/unnecessary (my side) and a group decreeing their political views as undeniable truth or standards for the forum. Aside from no consensus on those views, prior metas on these things showed that even those people believed our standards would be defined by what we spoke for and against with silence itself being a vote for something. So, a few of us with different views on political angle, who still opposed the comment, had to speak to ensure the totality of the community was represented. It’s necessary as long as (a) we do politics here and (b) any group intends to make its politics a standard or enforeable rule. Countering that political maneuvering was all I was doing except for a larger comment where I just answered someone’s question.

                                                  Well, that plus reinforcing I’m against these political angles being on the site period like I vote in metas. You can easily test my hypothesis/preference. Precondition: A site that’s usually low noise with on-topic, productive comments. Goal: Identify, discuss, and celebrate the achievements of women on a list or in the comments maintaining that precondition. Test: count the comments talking about one or more women versus the gender identity of one (aka political views). It’s easier to visualize what my rule would be like if you collapse Derek’s comment tree. The whole thread meets the precondition and goal. You can also assess those active more on politics than the main topic by adding up who contributed something about an undisputed woman in CompSci and who just talked about the politics. Last I looked, there were more users doing the politics than highlighting women in CompSci as well. Precondition and goal failed on two measurements early on in discussion. There’s a lot of on-topic comments right now, though, so leaned back in good direction.

                                                  Time and place for everything. I’d rather this stuff stay off Lobsters with me only speaking on it where others force it. It’s not like those interested can’t message each other, set up a gender identity thread on another forum, load up IRC, and so on to discuss it. They’re smart people. There’s many mediums. A few of us here just want one to be better than the rest in quality and focus. That’s all. :) And it arguably was without that comment tree.

                                                2. 8

                                                  So, I avoid bringing this stuff up much as possible.

                                                  Keep working on this

                                                  1. 2

                                                    The dont-rock-the-boat, kinder approach wouldve been for person rejecting the gender claim to just ignore talking about the person he or she didnt think was a woman to focus on others. The thread wouldve stayed on topic. Positive things would be said about about deserving people.

                                                    Do you believe the most deserving will be talked about most? If you have a population that talks positively about people whether or not they are trans, and you have a smaller population that talks only about non trans people and ignores the trans people, Which people will be talked about most in aggregate? It isn’t kinder to ignore people and their accomplishments.

                                                    It is also very strange for technology people to reject a technology that changes your gender. What if you had a magic gun and you can be a women for a day, and then be a man the next, why the hell not? We have a technology now where you can be a man or a women or neither or both if you wanted to. Isn’t technology amazing? You tech person you!

                                        1. 2


                                          This has nothing to do with cognitive science. It’s about computer processing of speech and natural language.

                                          1. 1

                                            Language and speech are handled by cognitive processes.

                                            1. 2

                                              Language and speech are handled by cognitive processes.

                                              In humans, not in computers.

                                          1. 4

                                            Can we please have a tag for posts to sites that require you to have signed up before they can be read?

                                            1. 2

                                              AIUI such stories don’t belong here anyway.

                                              In this case, you can click “not now” or even use browser devtools to delete the annoying popup.

                                            1. 2

                                              Can we please have a tag for posts to sites that require you to have signed up before they can be read?

                                              1. 3

                                                I want to know about the people who don’t follow everybody else, like sheep. Who were the most down voted?

                                                1. 5

                                                  I don’t actually think this means what you think it means, at least if people are using down votes the way I’d like to see them used.

                                                  For me, a down vote means “This has no place here”.

                                                  1. 3

                                                    At least on HN and TrueReddit, which I think share your (and my) preference for how downvotes should be used, downvotes seem to be abused to reflect disagreement maybe 2/3rds of the time. It’s a shame, but seems inevitable.

                                                    1. 4

                                                      Exactly. Sometimes I also think people view downvoting as their way of saying “feh” to someone whose ideas they somehow disapprove of or deem unworthy.

                                                      IMO such a disagree/disapprove downvote is a major cop out. Either reply and explain yourself or upvote someone who’s already done so that you disagree with.

                                                      1. 4

                                                        If people can up-vote without having to post a reason, what is wrong with down-voting without posting a reason?

                                                        There are lots of reasons for down-voting, including “This has no place here”.

                                                        1. 5

                                                          Arguably we should have the mechanism to document reason for upvotes.

                                                          But, downvotes without reasons are a malfeature. That mechanisms encourage the level of discourse one finds at HN and Reddit.

                                                          We at least attempt to do better.

                                                          1. 3

                                                            Because in my view, the system here is designed to measure merit.

                                                            If I think an article is interesting or useful, I upvote it. If I don’t, I simply leave that article alone. No negative action is required.

                                                            We DO need a mechanism for keeping what’s posted here in line with the kind of thing the community wants to see, and that’s where I see down votes coming in.

                                                            Think of Lobsters as a bar graph, with the most voted for articles bubbling to the top and generating the longest bar.

                                                          2. 1

                                                            At least on HN and TrueReddit, which I think share your (and my) pref

                                                            People can disagree on what things constitute that which has no place here

                                                            1. 1


                                                              What’s that?

                                                              1. 2


                                                                (Don’t use it myself.)

                                                          3. 2

                                                            I deliver niche content, thank you! I’d have piles of funding by VC’s and on Kickstarter if I stayed on popular topics in popular places. I imagine some others, too. Most of us are here on this specific forum for stuff better for the brain, though. ;)

                                                            Far as most downvoted, it’s gotta be that libertarian fellow: I’m often expanding their comments to see exactly what was said. Usually just some ideological repetition but every now and then a good counterpoint.

                                                            1. 1

                                                              How about having a count of our yearly total up/down votes, with an option to make them public?

                                                              1. 1

                                                                I’d almost rather limit the number of downvotes that people can cast in a given time period to remind people that a downvote is more censure than disagreement.

                                                                1. 1

                                                                  I think a limit on both up/down would be good. It would certainly make me spend more time considering whether a link really was worth an up-vote.

                                                                  1. 1

                                                                    I dunno. I think upvotes should be easy, downvotes should require due consideration.

                                                              1. 1

                                                                Yeah, they’re interesting since they use rewriting logic in K and Maude instead of traditional proof assistants. One use of Maude was finding errors in SCOOP model for concurrency that Eiffel uses. The language work ranges from Scheme to Prolog to C with the semantics of latter into a compiler. If I picked one, I’d have this group do the semantics for Rust with C as the output leveraging their existing work. That could solve a lot problems in terms of reusing tooling.

                                                                Their recent work is the company hosting the submission with the static analyzer for C programs with no or few false positives being most notable. It’s a cool group. I was glad to see on this submission that they’re porting K to LLVM for performance enhancement.

                                                              1. 8

                                                                Lots of books on the coral reef these days! I get all my programming book recommendations from this community, so here are some titles from other areas of my reading life that have crustacean appeal.

                                                                Two tech history books:

                                                                Two books on contemporary technology:

                                                                And two novels:

                                                                • Nova by Chip Delany. Finally read this classic from 1968 and there is so much to chew on in 2017: post-work economics, cyborg spinal interfaces, race and racism after interstellar travel.
                                                                • The Devil in Silver by Victor LaValle. Creeped-out horror set in a modern-day psychiatric hospital that flips “Cuckoo’s Nest” on its head.
                                                                1. 2

                                                                  Anymore book recommendations on the topic of computing history ?

                                                                  1. 3
                                                                    1. 2

                                                                      Sure! :) Computer: A History of the Information Machine by Martin Campbell-Kelly and William Aspray is a drop-dead classic. (The first edition came out in 1996 but they’ve since updated and expanded the book with contributions from other historians.) Or, for a deep dive on a single machine with an unusual story, check out Now the Chips Are Down, a history of the BBC Micro by Alison Gazzard.

                                                                  1. 4

                                                                    I always list the best I read during the year as my Christmas book list.

                                                                    1. 3

                                                                      Awesome! Had to check book tag also since 2016 & 2017 are tagged books.

                                                                      1. 2

                                                                        Thanks. Your comment prompted me to make the tags consistent, e.g., book vs books, or even Just Christmas. So the other yearly suggestions are now listed on the same tag :-)

                                                                    1. 10

                                                                      I was curious as to how this bug could have occurred and found on the compcert c page that

                                                                      This part of CompCert (transformation of C source text to CompCert C abstract syntax trees) is not formally verified.

                                                                      So it seems CompCert C’s guarantee is a bit weaker than

                                                                      the generated executable code behaves exactly as prescribed by the semantics of the source program

                                                                      as claimed on http://compcert.inria.fr/

                                                                      And it’s more like, “the generated executable behaves exactly as prescribed by the semantics of the AST we parse your C source program into”

                                                                      1. 4

                                                                        Right: the bug was actually in the parser, not the compiler proper. Maybe I should edit the title?

                                                                        Seemed like a big deal anyway.

                                                                        Edit: Noted parser in title.

                                                                        1. 6

                                                                          http://compcert.inria.fr/man/manual001.html#sec10 shows the project structure, and claims the parser is in fact verified.

                                                                          Edit: https://xavierleroy.org/publi/validated-parser.pdf has the full story on the verified parser. In brief, it’s verified with respect to an input grammar. Which, in this case, contained an error.

                                                                          1. 5

                                                                            [CompCert’s parser is] verified with respect to an input grammar

                                                                            If that’s so, why doesn’t the commit that fixed this bug contain a change to the grammar or the proof?

                                                                            1. 3

                                                                              A look through the patch shows I was wrong about it being a grammar bug. Those do happen, but the actual cause of failure was a little more complex here. I should be more careful about speculating out loud!

                                                                              All the changes were in the “typed elaborator” phase of the compiler, which takes the raw parsed AST into the type-annotated AST that is the top of the verified stack. It seems like a basic error when handling variable scopes that is triggered by the shadowed variable names.

                                                                              Formally reasoning about scope extrusion is difficult and tedious… but I bet verifying the typed elaborator just rose a little higher in the CompCert development priority queue.

                                                                            2. 4

                                                                              Deleted my other comment since I didnt know parser had been verified. My bad. Related to it, I will say the tally of bugs found in specs vs implementation will remain interesting as the weakest version of the proof says the implementation will be at least as accurate or failed as the specification. The Csmith bugs were spec errors IIRC that the implementation faithfully followed. ;)

                                                                              Anyway, such results continue to remind folks formal methods need to be supplemented with other verification techniques.

                                                                            3. 2

                                                                              I’m being pedantic, but the “runtime error” occurred in a program that was compiled by CompCert (and its parser), so the title still isn’t really accurate. (Just saying “error” would be enough…)

                                                                              1. 1

                                                                                Hey, no better venue for pedantry than a story like this. :-)

                                                                                I’d edit the title again, but I can’t. I’d speculate that there’s some kind of time limit or score threshold on title edits… not going to go read the Lobsters source to find out exactly, though.

                                                                            4. -3

                                                                              Formal methods is so intellectually dishonest.

                                                                              Once I have a translator for language-X, I can claim to have created a formally verified compiler for that language, using the same arguments made by the authors of the Compcert papers.

                                                                              Papers involving formal methods should have to pass the same truthfulness and accuracy requirements as soap powder adverts: http://shape-of-code.coding-guidelines.com/2013/03/10/verified-compilers-and-soap-powder-advertising/

                                                                              1. 9

                                                                                You can’t claim to have created a verified compiler until you have a formal semantics of source, of target, a spec of your transformations, and proof they do what they do. It’s so hard they started with mini-Pascals before working up to C subsets (eg C0->TALC) to the subset in CompCert. There’s also semantics by another team to catch undefined behavior.

                                                                                So, you just made that crap up with no evidence. Further, what empirical evidence we have by looking up data in the field shows verification works at reducing defects in various parts of lifecycle. Far as CompCert, Csmith empirically confirmed the CompCert team’s claims of strong defect reduction when they through tons of CPU time at trying to find defects. They found just a few spec errors in CompCert but piles of errors in others. Regehr et al were amazed by its quality.

                                                                                Comments about worth of formal methods should have to use the scientific method or something when making claims. In this case:

                                                                                1. Define correctness requirements for compilers. There may be several.

                                                                                2. Assess how well various compilers met them, how often, and developed with what methods

                                                                                3. Determine if formally-verified compilers achieved higher quality than those without it. Also, compare to other QA methods such as code review or unit testing.

                                                                                CompCert passes across the board with such criteria. Not that I still want, as in EAL7 requirements or DO-178C, to throw more exhaustive testing and review at it to check for any errors in specs. I wont rely only on one method as empirical data says use diverse array for highest confidence. It’s already orders of magnitude better in defect rate than other compilers, though.

                                                                                1. 2

                                                                                  Formal methods is so intellectually dishonest.

                                                                                  I think you mean the compcert people.

                                                                                  Once I have a translator for language-X, I can claim to have created a formally verified compiler for that language, using the same arguments made by the authors of the Compcert papers.

                                                                                  I think you can only claim that starting from the C code, that what your frontend produces will be as faithfully be converted to machine code as what is technically possible using the best technology available.


                                                                                  To your articles point about undefined behaviors, I’m pretty sure it is possible to prove absence of those problems in C code using frama-c and acsl. The problems will always be pushed to the boundaries until you have done this for the entire system.

                                                                                  1. 0

                                                                                    I think you mean the compcert people.

                                                                                    No, I mean formal methods people in general. The compcert people have done some interesting work, but they are not advertising what they have actually done.

                                                                                    … undefined behaviors, I’m pretty sure it is possible to prove absence…

                                                                                    I’m not sure about proving, but it should be possible to get a high level of confidence.

                                                                                    Yes, there are tools to do this, but compcert did (still does not?) use them (or do it itself these days?).

                                                                                    1. 3

                                                                                      Try using frama-c with -wp-rte plugin to see what I mean about runtime errors. compcert compiles valid C, other tools help you write valid C.

                                                                                      1. 2

                                                                                        “ The compcert people have done some interesting work, but they are not advertising what they have actually done.”

                                                                                        The papers I read note the specific goals, limitations, and techniques used in their methods. They did publish a lot of stuff. Maybe I missed something. What do you think they’re lying about in what papers about the CompCert tool?

                                                                                        “No, I mean formal methods people in general”

                                                                                        Much of the formal methods literature done by pros lists their specific methods plus their dependencies and what parts can fail. I rarely see people outside the formal methods community talking reliability or security do that. Looking for “TCB” is actually one of techniques I use in Google searches to find the papers I submit. It’s that rare for it to pop up in papers outside either formal methods or high-assurance systems despite it being foundation of their claims.

                                                                                        There’s certainly zealotry to call out. There’s certainly problems with peer review or reproducible results. These are true in most if not all sub-fields of CompSci. Maybe for experimental science in general since a lot of article in recent years are complaining about non-reproducible or fake research. For some reason, though, you only bring it up on formal methods threads. I wonder why you find the other threads acceptable with their imprecise and/or non-reproducible claims but drop in a formal methods thread to throw under the bus researchers who note strengths, weaknesses, and dependencies plus publish quite a bit of source code. Quite a double standard you have, Sir!

                                                                                1. 4

                                                                                  Some useful links:

                                                                                  DIS stands for Draft International Standard.


                                                                                  Hashes of archived n4660.pdf:

                                                                                  CRC32:  0e229cd7
                                                                                  MD5:    3cc1c1c0f4a3a969d44d699f710a7907
                                                                                  SHA1:   99cbb72495fae9d5376e84d191d0ed37ffdac74c
                                                                                  SHA256: 1706ca84c49a83a6da5bb0557e044fe9a5d6788685439a04bc793a077e6c71d3
                                                                                  SHA512: bfa1032ccbd46a6cb7be969476febc519883198da1bf97763b13f92554412f260712db5ad2d7e6bfd763a4c33c0d087f72a7271118b3e0597a45b1ea356e7266
                                                                                  1. 6
                                                                                  1. 2

                                                                                    The barrier to entry is very low, the companies pushing their tools try to make it as easy as possible to get an answer (any answer).


                                                                                    1. 1

                                                                                      Another issue is the quality of training they give. I attended a tensorflow training at a conference and they only went through 3 examples in 3 hours. All that could be gotten from their basic tutorial.

                                                                                    1. 1

                                                                                      The curves for compile time and binary size are double exponential, $size=e^{e^{a*Level}}$, where a is 0.79 for compile time and 0.12 for binary size. Not sure why the author thought a single exponential looked like a good fit.

                                                                                      R code:

                                                                                      plot(csh$Level, log(csh$Compile_Time), log="y")
                                                                                      c_mod=glm(ll_CT ~ Level, data=csh)
                                                                                      b_mod=glm(ll_BS ~ Level, data=csh)

                                                                                      Data extract from table:

                                                                                        1. 1

                                                                                          perhaps for free programming books but this list includes much more than free and much more than programming. But then again, I am a sucker for a good book list.

                                                                                          1. 1

                                                                                            That one is sadly only focused on Programming. :(

                                                                                          1. 3

                                                                                            All methods work if you are willing to spend enough money.

                                                                                            If only clients would stop asking for low cost, low defect and short timescale, then software developers would stand a chance of delivering what was wanted.

                                                                                            1. 1

                                                                                              This article is an accurate description of the PPIG work. I attended a couple of PPIG workshops and was active on the ppig mailing list for 16 years (I was booted off for not willing to be politically correct), while working on a book that tried to apply cognitive psychology to language use pdf available here.

                                                                                              “The Psychological Study of Programming” by B. A. Sheil, from 1981, says the same about psychology of programming research in general (cannot find an ungated copy).

                                                                                              The main problem is that few of those involved have ever studied psychology (which has very good experimental practices, at least in cognitive psychology).

                                                                                              1. 2

                                                                                                More excellent sleuthing on software engineering claims in his very readable book The Leprechauns of Software Engineering.