Golang, some first feeling.

I am using golang since some months, mostly for exercise, and after a while I would like to share some balance of this period. I hope a nice discussion can start. I used to develop in C, C++ and ADA95, since I was doing HPC and some part or railways consulting. After I changed becoming an infrastructure person: architecture, WAN, and so on. So i mostly wanted to keep in touch, and learn a modern-design programming language. <h2>PRO:</h2> I've to say, is fun. Really. I gave myself a goal, to write a server which provides an NNTP interface and uses P2P to propagate posts and groups. (Useful or not, you need a challenge). It took 3 weeks of my spare time (not so much, then) to develop a NNTP server working with slrn, soup, thunderbird and pan. Amazing. I could release it as a local NNTP server. I am still into the P2P part. Learning curve? Good. Not a single library: I just used go and its libraries, and the NNTP RFCs , and the more I wrote, the more I reused. Amazing. I started to use it as a "c", only writing functions and passing arguments. Now I am into goroutines, and entering the planet of interfaces. I was missing ADA95 templates for safely accessing data, but I see interfaces here. golang looks like C+++, plus boost, plus some features from ADA. Looks like they did it for me.... :) Joking apart, the fact I could achieve a NNTP server in , like, 3 FTE, was impressive, given i was not programming since years. <h2>CONS:</h2> I think the community should be refocused, or at least improved. Don't take me wrong, I am not willing a fight. But. Ok, golang has pointers, cycles, idioms, and so on. All that basic stuffs are good to study. At school. Having 60% of posts around like "how to use struct", "how to cycle", "how to pass arguments", is terrible. It makes people looking for some suggestion to waste time. Like you want to know abou tcp sockets and you are lost in a immense "Hello World" grass field. You should have learn "hello world" at school. I think the community should focus more about what is really the issue of go (interfaces, goroutines, and so) and leave the common things to the school. The schools people is supposed to have before of powering up a computer. At the end, developing is not a kind of welfare supposed to give an income to everyone: is a job. You should have some basic skills before of applying. Another cons is the "dev for the show". Programming as a new welfare. People writing libraries on github just to have a new line on Linkedin. Not maintaining them, not fixing bugs, and so on. Just an example: We developed a framework in my company. It took a team of business analysts to get a coherent set of use-cases out of 3,000 customers (mostly enterprises: is there another kind of framework user?). Then a team of developers coded and did formal verification. And then a team of technical writers wrote the documentation.It took 2 years. Now, I see single people with no customers, programming alone, to come and say "I wrote a framework last week". No. Forget it. You don't.You didn't . You can't. End of story. Somebody should stop that. Because other people then will start using those "wannabe-frameworks". Expecting they are frameworks. And the result will be on newspapers as the "security leak of the year". The same for libraries. Writing a library is not an easy job. Documentation has to be excellent, since who uses the library should know to invoke the API, but is not sufficient. Should also know when NOT using it, how it performs and its limits. I found a ton of "libraries" which have no documentation at all, just "how to invoke it". The first version of my program crashed after 11 hours of running, just because the UPnP library was opening UDP sockets and never closing them. And it was logging in chinese. And it was "THE" library for NAT-UPnP. Everybody is suggesting this library. I tried to contact the developer and he didn't answered: he had its line on its linkedin profile, so mission accomplished. So half of the "planet go" is using a NAT UPnP library which crashes after some hours. I went to NAT UDP , at least I see a RFC for that: but still the issue is: once one library is written, everybody is suggesting this library. And there is no rating. And people is writing them just to enrich their linkedin profiles. Heartbleed was not enough as a lesson? Too many people is writing their "package" or "library" just to add one line on their resumee , to appear good to the human resources. They throw some bullshit on github, they forget it, and they're done. One more line on linkedin. So we have a ton of "restful framework for web applications scaling well with rest and mongo/couch in the cloud". To better hit the top-10 buzzword list, i guess. When I was young we had buzzwords like "fractals, chaos theory, quantum computing and neural network" mentioned: maybe those buzzwords are a bit outdated, but I still see "buzzword-as-a-welfare". I think the community should react to that, starting to rate libraries and "frameworks". this "i wrote a framework just because I want to give a talk" or "I wrote a library for my linkedin profile" will poison everything. To find a reliable library is close to impossible right now, and go is at the beginning of its life. Worst , after one library is written, everybody suggests to use this to the others, so no better libraries are developed.The terrible NAT-UpNP library I was using had thousands of forks. One per bug, I guess. Again, heartbleed was not enough as a lesson? Last but not least: golang comes with an impressive amount of libraries. Amazing. Most of people talking of go are talking about pointers, reference, loops, functions... topics which are not go-specific. So you learn to write a routine in the same way you could write in c, java, php and python. And you don't get something: there was already some go package doing that. In one line. Again, I think the community should focus more on go-specific issues. Comparing a language to others is a futile discussion. Answering to people which says "java is faster" is a waste of time. To show how to use crypto libraries which are coming with the go compiler is more, and more, and more interesting. When I was looking around how to truncate a string, I found a load of c-like routines with loops. Then I dig into the go-specific features, and I see a stupid line was enough: but is not c-like, is go-like , and perhaps go-specific. So I think the community is still in time to focus more on go, less in pseudo-framework, pseudo-libraries which are not (neither can be) what they claim to be, and focus on explaining go-specific issues. How to write a "for" statement should be clear much before of starting to program, IMHO. Just my two++ cents. <hr/>**评论：** slimsag: <pre>Your pros seem pretty cool, looks like you got to experience a good amount of the language/ecosystem (and in three weeks, no less!) :) Most of your cons don't seem to be about Go in specific but more about your perspective (or rather ideals) about software development in general. <blockquote> Ok, golang has pointers, cycles, idioms, and so on. All that basic stuffs are good to study. At school. Having 60% of posts around like "how to use struct", "how to cycle", "how to pass arguments", is terrible. ... How to write a "for" statement should be clear much before of starting to program </blockquote> I haven't seen many articles about that, past maybe Effective Go and example code. Everything I've seen is about more advanced Go patterns like channels, goroutines, etc. Also consider that most people are just being introduced to programming, and there should be no requirement on a formal CS background to simply learn how to program -- we're in the 21st century for a reason: learning can occur in person or online. <blockquote> Now, I see single people with no customers, programming alone, to come and say "I wrote a framework last week". No. Forget it. You don't.You didn't . You can't. End of story. Somebody should stop that. Because other people then will start using those "wannabe-frameworks". Expecting they are frameworks. And the result will be on newspapers as the "security leak of the year". once one library is written, everybody is suggesting this library. And there is no rating. And people is writing them just to enrich their linkedin profiles. Heartbleed was not enough as a lesson? </blockquote> Anybody can write a framework, or library. They can publish it to the internet, and others are allowed to recommend it. We're not a totalitarian community, nor should we be. The lesson from OpenSSL's Heartbleed was that people like yourself blindly accept someone else's code as "correct" when it may not be. If you don't understand how 100% of OpenSSL's source code works, then you are trusting the person who wrote that code. The same applies to many situations of life. We all want perfect libraries that work for everyone's use case, but the only way we're going to get there is by learning from our mistakes and trying a lot. Research your libraries and personally ensure that they do what you want, or else you accept the risk of trusting that the person who wrote them knows what they were doing.</pre>Low-Eel: <pre><blockquote> Your pros seem pretty cool, looks like you got to experience a good amount of the language/ecosystem (and in three weeks, no less!) :) </blockquote> Well, the goal was pretty ambitious. I wanted to write innd+bittorrent+dht , and It was fun. When is fun, you dig in. But also, you google a lot. I was a newbie. <blockquote> Most of your cons don't seem to be about Go in specific but more about your perspective (or rather ideals) about software development in general. </blockquote> 100% true. I agree on that. But golang is "special", because is new. As I wrote, it is still possible to fix this, and make go REALLY different. <blockquote> we're in the 21st century for a reason: learning can occur in person or online. </blockquote> This is probably the part I don't agree. getting information and getting education is different. Behind any tecnique there is some theory. Of course you can feel a cowboy and ignore the theory, like people going with perpetual motion. But the theory will make you pay the price. Like, perpetual motion will never work. Sooner or later, the theory you never studied will present you a fee: you waste time. <blockquote> Anybody can write a framework, or library. They can publish it to the internet, and others are allowed to recommend it. We're not a totalitarian community, nor should we be. </blockquote> I am not asking for censorship. One solution could be rating. Like google play have . I won't say this is sovietic. i would like to write in some places that a library cannot panic a whole program, that a library should close any file descriptor it opens , or have a method to do it, and then this UPnP library is bullshit. But I can't. And when I asked for suggestions, this was depicted as THE library for NAT UPnP. If you don't like rating, ok, so we have a technical solution already: formal verification. I f you want to stay "tecnical", yes, I ask to provide the golang "testing" feature with formal verification capabilities. <blockquote> The lesson from OpenSSL's Heartbleed was that people like yourself blindly accept someone else's code as "correct" when it may not be </blockquote> No, the problem was much, much bigger: this SSL library was trusted because , googling around (like you mention: learning online) everybody was telling around "this is the library", "it comes from OpenBSD people", and so on. The trust was not a "blind" trust: was a immense BIAS. If anybody was reading almost ALL the literature in the planet, it was telling you "this is safe, this is the best". Only developers which have ACTUALLY tried to use OpenSSL noticed it was a bullshit of incoherent interfaces. But they had no chance of telling it. Don't depict the trust being "blind": there was a shit load of endorsement by "experts" on this library. And no formal verification. It is very, very easy to proof heartbleed would not have passed a formal verification process. So yes, I think I am asking a formal verification tool for go. Yes, it can go. I am not havin "ideals" about development, btw: as a company we are asked to formally verify everything. It is business and pretty normal in automotive/railways. <blockquote> We all want perfect libraries that work for everyone's use case, but the only way we're going to get there is by learning from our mistakes and trying a lot. Research your libraries and personally ensure that they do what you want, or else you accept the risk of trusting that the person who wrote them knows what they were doing. </blockquote> The easiness of developing in golang makes then useless to use libraries. It was faster to me to write NNTP from scratch than debug someone else library. So, we don't need frameworks or libraries, only software. Which is a suitable position, don't take me wrong. If this is the case, why I see people announcing its need-to-be-debugged frameworks everyday, when it takes more time to debug than to rewrite from scratch? Good question. What I suggest, exactly? <h2>Being honest, I would see the "testing" feature of golang a bit more powerful, putting formal verification in it.</h2> This is the only solution I see, being honest. To see a very good language being covered of bullshit in a few monts is very , very, very sad. Maybe just because I like it.</pre>jimuazu: <pre>Formal verification would be really interesting. What kind of formal verification tools/languages/etc do you use in other languages? How hard would it be to adapt one of these for Go?</pre>Low-Eel: <pre>Well, we are mostly using Frama-C with ACSL The issue is more or less this: <a href="http://www.adacore.com/knowledge/technical-papers/testing-or-formal-verification-do-178c/" rel="nofollow">http://www.adacore.com/knowledge/technical-papers/testing-or-formal-verification-do-178c/</a> and you can find it here: <a href="http://frama-c.com" rel="nofollow">http://frama-c.com</a> and for ACSL: <a href="http://frama-c.com/acsl.html" rel="nofollow">http://frama-c.com/acsl.html</a> As you can see, it is quite a work, if you want to reach 178C, which is , I would say, "a bit too much" for amateur software, :) :) even if, with IoT, I would not wonder if something similar would be requested in the future on all IoT. I tool I prefer (but I am not developing since year, I am mostly into TRAC architecture) is <a href="http://spinroot.com" rel="nofollow">http://spinroot.com</a> <blockquote> How hard would it be to adapt one of these for Go? </blockquote> As far I remember, there is a tool which translates go to C (maybe is the other way around?) but I never went deep in it. Converting go to c would permit to use spin, by example. And also go is high-productivity-oriented, so I can't say to add such an analytic work. But I can think to port "some ideas" to golang. Not all the framework, just a little piece. What I would like would be something added to the test framework, which permits me to write "comments", like: <code> @@ assert (__net.Conn# == 0 && __filedesc# == 0) </code> meant that in this point we have no sockets open and no files open. Then, when I import a function i can "lock it" like: <code>@@ assert (__net.Conn# == 0 && __filedesc# == 0)</code> <code>myforward := new(UpNp)</code> <code>@@ assert (__net.Conn# == 0 && __filedesc# == 0)</code> this would mean that before and after this call, I expect there are no file open and no socket open. Then, some test framework could check if this happens or not. This would solve many problems when writing and when importing This is not a full verification, neither a verification at all, I am just importing some ideas I've seen, but could be very very useful: imagine I expect at a certain pont a < 10 and a > 2, just write it as a comment, and some test tool can check if this happens. Just my two cents++, of course.</pre>klaaax: <pre><blockquote> Now, I see single people with no customers, programming alone, to come and say "I wrote a framework last week". No. Forget it. You don't.You didn't . You can't. End of story. </blockquote> edited for politeness purpose, bottom line is , you're not entitled to anything, and people do not work for you. people use github and co as free hosting for their project. So stop being arrogant because you think you're a "real programmer", you must be really a pain to work with, I pity your poor colleagues having to work with a jackass like you . If you find a bug , make a pull request, if you think something is done wrong, then open an issue but don't come here and complain people are writing software you don't want,they do it for free. They do that for various reasons and you don't get to judge them. Seriously , you're the worst person in the world , and I'm really shocked someone can say something like that. What the fuck ? really ? read your message again . I don't want anybody like your kind in the go community , please go away.</pre>leuro: <pre>You wrote fXXX I wanted to write if I could use proper English, thank you.</pre>jimuazu: <pre>I think the point is that there is a general culture of lower expectations of quality ("it runs, ship it!") -- at least lower than some other languages or fields -- and that people recommend buggy projects as the best ones. It is true, what can you expect? Many new people coming to Go generally haven't the experience to know otherwise. I have exactly the same feeling going from a project with high standards and effective code-review to one where everything is more lax and standards slip and the whole project is constantly paying for it in terms of debugging and fixing avoidable bugs. Why don't they see that they are creating these problems for themselves? But it is cultural -- what can you do? If you try and change the culture (as this guy is trying to do) people don't like it much. Better just accept it and don't use low-quality 3rd party libraries that don't have a history of fixing bugs or accepting patches.</pre>klaaax: <pre>it's not like go doesn't have tools to assess the quality of a project tests? code coverage ? vetting and linting ? all built in Go. And it's not like people can't interact with authors on github and co. </pre>natefinch: <pre>It sounds like you got burned by using a bad library. That's unfortunate. But go is a relatively new language, and NAT uPNP is not exactly an everyday technology to use, so I'm not surprised that there's only one semi-complete library for it right now. Heck, I'm kind of surprised there was a library for it at all. I don't think there's anything wrong with people noodling around with a language to get a feel for it. We've all done it. You did it. You can't just trust that some repo on github is quality code. You have to dig in and check for yourself. Run <code>go test -race -cover</code> ... are there data races? Is the code coverage better than ~85%? Are there issues filed weeks or months ago with no responses? If there are hundreds of forks, why is that? How do they differ from the original? Read the code. Are there docs for every exported type and function? Is the code easy to read and well organized? Does it clean up after itself (defer f.Close etc)? Read the tests, are they easy to understand? Are they thorough in their attempt to cover all use cases? I think a rating system for Go packages would be good... but that's a non-trivial exercise to put together and make trustworthy. Your idea for formal verification is really only applicable to packages that implement well-known standards. You can't formally verify my log rotation package, for example - it's not implementing a spec. That's what tests are for. Your post comes off as pretty grumpy, and is not really a very good first impression to give the community. You say the community needs to change, but it seems like maybe you need to change a little too. Don't be so grumpy! :) People are coding in Go and having a good time doing it. That's awesome! They're writing code with this language and feeling their way through its nooks and crannies. Not every weekend sideproject can be a replacement for OpenSSL (or whatever). Sometimes you just want to hack together some dumb library to try out an idea you had in the shower.</pre>jimuazu: <pre>How about self-classification, i.e. encouraging people who publish code to rate it as "alpha", "beta" or "stable". Then there can be meaningful discussion about whether the code meets the classification without discouraging people who just want to put stuff out there in the open-source style of sharing/cooperation. It is still valuable that people put out "alpha" code because someone else might build something much better from that starting point.</pre>Low-Eel: <pre>Of course, for me would be very nice. I mean, my software has "STILL IN PROGRESS" label. But we should understand people is writing code to have another line on their linkedin profile. So they don't like to say "i wrote a beta". They want to write in the Linkedin that "they wrote the new amazing 42". This is the point I am noticing. And this is, IMHO, the point which made other languages a mess to use.</pre>Low-Eel: <pre><blockquote> It sounds like you got burned by using a bad library. That's unfortunate. But go is a relatively new language, </blockquote> Well, actually not just one. Initially I planned to use several libraries, and on 5, 4 were mostly JBOD. <blockquote> and NAT uPNP is not exactly an everyday technology to use </blockquote> well, if you want the router you have at home to open a tcp port thru the NAT, what you do? It seems to me most of home routers are using it. Anyway it was good, because it showed me golang doesn't needs so much libraries, often is faster to write them by your own than debug other's ones. <blockquote> I don't think there's anything wrong with people noodling around with a language to get a feel for it. We've all done it. You did it. </blockquote> I am not going around to say people can use my code as a library for NNTP or whatever. Sure, I am writing beginner's code, but I don't pretend others can reuse it. What had made me astonished was not "a library is bullshit". What mades me astonished is, when I ask for a UPnP library, everybody suggests to me this one. Which is very dangerous, if you think to OpenSSL and heartbleed. <blockquote> You can't just trust that some repo on github is quality code. You have to dig in and check for yourself. Run go test -race -cover ... are there data races? Is the code coverage better than ~85%? Are there issues filed weeks or months ago with no responses? If there are hundreds of forks, why is that? How do they differ from the original? Read the code. Are there docs for every exported type and function? Is the code easy to read and well organized? Does it clean up after itself (defer f.Close etc)? Read the tests, are they easy to understand? Are they thorough in their attempt to cover all use cases? </blockquote> all that you mention takes more time than writing it from scratch... this is the point. I am astonished by the amount of rest libraries are around, and actually, it is much easier to rewrite them from scratch than to follow all checks you mentioned. So if we proceed that way, given the high productivity golang achieves, we don't even need libraries. The other alternative (to write them from scratch) is a time saver. This is why I say: ok, let's have a formal verification tool. So we can test formally the library, and we don't waste such a time to debug other's code. I think we agree to debug other's code takes a terrible amount of time, right? <blockquote> You can't formally verify my log rotation package, for example - it's not implementing a spec. That's what tests are for. </blockquote> And how can I know it won't crash my program, or that is not a waste of time to use it? I am just doing it for fun, but if my time was paid, I won't spent it on each log rotation library I find. It is probably faster to write one from scratch. This is the point. <blockquote> Your post comes off as pretty grumpy, and is not really a very good first impression to give the community. </blockquote> Well, actually I started with the good feeligs, and perhaps, at the end, I just would like to have an automatic formal testing tool. As I said, I am starting to develop just for fun thanks to golang, after 10 years. I won't say this is "grumpy", eing honest. But also I see some issues which needs, IMHO, to be addressed. Actually I won't have spent a minute of my time, if I was grumpy: grumpy people just says "that's bullshit, I go home". I never had seen a grumpy employee coming and say "I would like to have a tool for this and that". In my experience, they only mourn in the caffee room....</pre>natefinch: <pre>It sounds like you want some magical tool that will tell you that a library is good or not. I think <code>go test -race -cover</code> is the closest you're going to get. It's just not possible to write a tool that can determine completeness and correctness of arbitrary code. How do you use third party code in other languages? It should be the same for Go. Go isn't special in regards to there being more bad code out there than good code.</pre>Low-Eel: <pre>Again: I want to check a software against a policy I write. Which means , you are free to write what you want, but I am also free to check if it meets MY OWN policy. Of course people will write software according with THEIR policy. Which they are free to do. But also, I want to be free to understand if the software meets MY policy. Where "MY" could be my own one, or the customer's one. Which is an issue.</pre>szabba: <pre><blockquote> well, if you want the router you have at home to open a tcp port thru the NAT, what you do? It seems to me most of home routers are using it. </blockquote> I think what <a href="/u/natefinch" rel="nofollow">/u/natefinch</a> was getting at is that most people don't write code where such a library is necessary or even useful.</pre>Low-Eel: <pre>Ok, but still, we have two problems: <ul> <li>Bias saying: "this is the library to use"</li> <li>A library which is forked and included in a couple of dozen of application (like also synthing) and have some huge flaws.</li> </ul> so, either we fight the bias, and stop saying "problem solved" each time a software pretends to do something, or we start checking the problem was actually solved. </pre>szabba: <pre>I don't thing formal verification is a solution for everyone (caveat: I've never used it) or even for most people. I agree there is a problem, but I think it lies mostly in our behaviour. Side note: your original post sounded demanding and at places demeaning to other people. Not everyone is going to want to discuss with you if that keeps up.</pre>Low-Eel: <pre>Well, if you say "golang is a better c" you should consider many and many formal verification tools came with C. Is hard to say "add formal verification to something which was designed with speed in mind", of course.But also, some "light" practices, coming from frama-c , could be integrated. <blockquote> Side note: your original post sounded demanding and at places demeaning to other people. Not everyone is going to want to discuss with you if that keeps up. </blockquote> well, when you complain because people is , by example, smokin where they should not, of course some people will feel pointed. When you complain against some convenient bad practice, you always get hate back. On the other side, if you want a bad practice to stop in a human group, you need to raise the problem, and get the hate back. Of course you could prefer to keep the bad practice, and don't wonder when the common environment becames a mess.</pre>szabba: <pre>"Go is a better C" is marketing. It's not a lie, just comes with small print -- in this case "for the kinds of work and situations it was designed for". And lack of formal verification tools is not a problem for most of them. I don't say there's not a problem in the community. I'm saying how you phrased your description was antagonizing. But enough of this. I'm not hugely affected by the issue anyway, so that's about how much time I'm willing to spend on it.</pre>dvirsky: <pre>You talk about some rating system for libraries. That's something I've been thinking about from the moment I first ran "go get". We do need some "pagerank for libraries". I know godoc.org has an algorithm for rating them. But most algos like this one use things like github stars, forks, how many other libraries import them, etc - that's a good estimation but it's not always enough. And it's a problem not exclusive to Go, of course. For example, things that are usually not ranked: how many 2nd degree dependencies does this library introduce? How do they rank (that's a recursive algorithm like PageRank)? How well does it perform (how do you measure that at all? compared to what?)? How good is the API? How well is it documented? How stable it is (maybe issues/clones is a good estimate)? Is it actively maintained (maybe a small library that just works and has no bugs doesn't need any further maintenance? I have a couple of those that I use but barely touch). And all these are just guesses - you'll miss on great libraries that go under the radar, and on the other hand bad ones will bubble up in their rank. But you're welcome to try and formulate some algorithm to estimate and rank libraries that is better than what's out there today. But I don't think people should stop themselves from publishing libraries. BTW I'm actually in the process of writing an API management framework, because the ones that are available were not on par with my company's needs, or were not maintained and documented well enough. And I'm contemplating whether I should open it or not (it's using a couple of 3rd party libraries, but not too much). It's turning out great, but it just feels to me like I'd just create noise for people if I publish Yet Another Rest Framework For Go. </pre>klaaax: <pre>Open source your stuff if you want to really. It's other people job to vet stuff not yours. You shouldn't feel like you need to hide your work because of idiots like <a href="/u/Low-Eel" rel="nofollow">/u/Low-Eel</a> who is a serious douche bag, one of the worse kind. On the contrary, good people will make constructive criticism about your work and might even contribute to make your framework better. Just don't let assholes stop you. You're not adding noise. It's not your job to do the vetting for others. You are contributing , unlike <a href="/u/Low-Eel" rel="nofollow">/u/Low-Eel</a> who is an entitled parasite of the worst kind. Hey but he has "3000 clients" so he's the king of the hill ! ... </pre>dvirsky: <pre>I'm not shy about publishing my stuff at all, if you look at my submission history you'll see a couple of projects for example. It's just the specific case of this rest framework. I'll probably open it though.</pre>Low-Eel: <pre>Well, not exactly. I was thinking something like that, just after the last reply. After a little discussion , it comes to my mind actually I would prefer a formal verification feature added to the "test" framework of golang. I think it could solve the issue, since then everybody can verify how good is a library before of using it. Rating is ok, but also rating is not that useful into industry, like it is EAL certification, by example. So I would prefer google to add formal verification into the "test" library I don't want to stop people doing the library, I want to save the time of people adopting them. A tool for formal verification could have saved my time pretty well, I think</pre>dvirsky: <pre>Formal verification will give me a good insight into the library's current stability, but that's just one factor when I'm choosing one. It won't promise me new features will be implemented, or that it performs well, or that the API that initially looks okay is in fact okay.</pre>Low-Eel: <pre>I am not saying formal verification can be the only criteria. But it could be quite a good MINIMAL requirement. Just for example, the heartbleed bug wouldn't have resisted to formal verification. Not that bad, right?</pre>dvirsky: <pre>I'm not an expert in formal verification, but wouldn't 100% test coverage, plus some fuzzer tests to cover various inputs, be close enough to what you're looking for?</pre>Low-Eel: <pre>I think there is a misunderstanding about formal verification: formal verification permits you to check a code against a policy you define. By example, to reach EAL5+ you could need to exclude dynamic allocation of memory, like for aircraft the standard 187C requires. But this is an example. The point is: people is free to write whatever they like, but you need some way to quicly evaluate if some software is compliant with some policy. Which is yours. So if you want to use a library, you can check it against your policy. To "test hard" is good, but actually is not like "I set my policy", or "my customer set the policy", by example. In automotive and railways, often the customers are doing that on their side. Also when you do ASIC or SoC, the foundry is doing that before of burning the silicon. So I can't understand why this seems that a terrible idea... </pre>peterbourgon: <pre>Formal verification is not a cure-all. It's incredibly laborious, and often in conflict with other important properties of software, like ease of modification, speed to produce new features, etc. </pre>Low-Eel: <pre>I didn't say it is a cure-all. We are working wiht automotive and railways, so I know how hard it is. But actually once you define a policy, you can reuse it automatically. And often is the customer itself to define it. And also I don't say it is mandatory for who writes all software. But, having defined a policy, I can check against this policy any library, and decide quickly. So this is an acceptance criteria, not a project criteria. I don't see using formal verification as a must for people writing software, I see it as a self defense for people willing to use code written by others.</pre>leuro: <pre>fuck</pre>

用户登录

今日阅读排行

一周阅读排行

最新主题