Chicago Police Department bought a sound cannon. They are going to use it on people.

stepinrazor · 9 days

Furthermore, why are devices designed with the intent of creating noise loud enough to cause permanent hearing damage not regulated by Geneva? Devices intended to cause vision loss are explicitly banned...

Because capitalism.

mck- · 9 days

You forgot to mention that editor means you get a nice class browser, a nice documentation viewer, a nice debugger, etc. It doesn't just mean being able to open up a file and edit a few lines.

ErisHeiress · 10 days

Unfortunately in their interactions with other companies they act like the typical corporation.

apfelmus · 11 days

Are you writing your formal specs using more advanced concepts like dijkstra's guarded command language or hoare logic or ...?

jdlshore · 11 days

Now, since I have a management background, I need to express myself in terms of Key Performance Indicators (KPIs). Formal proofs offer a better NCC/PCVE ratio ([number of cases covered] over [program correctness verification effort]) than whatever crappy methodology anyone may come up that disregards the essential fact that programming is mathematics.

Do you know of any papers that cover this or do you have stats/proof you can share? :S This would do a lot I think to encourage the use of it.

And they will continue to be expensive as long as legions of programmers are misled into adopting a hacker's mindset. Of course, formally proving the correctness of the archetypical program a hacker would write is terribly complicated - a hacker would treat a huge number of cases in ad-hoc ways, instead of looking for a single principle to unify them all. But an elegantly designed program does not have to be terribly expensive to prove - it is the explosion in the number of cases treated in ad-hoc ways which makes programs hard to reason about.

Precisely. I'm saddened that you were down-voted when the counter-arguments are so poor.

jdlshore · 11 days

Outside of some extremely niche industries, formal proofs are not used in professional software development.

They're not used but does that mean they shouldn't be used?

7500 lines of production C code took a team of 12 researchers four years to formally prove.

It's hard to formally prove something in a language that is relatively unsafe and not designed very well. It also looks as if they were writing the proof after the program was complete. Dijkstra covered that and encouraged writing a proof as the program was written.

I would also think that they had to do a lot of repetitive work. Some of the things implemented in that code I'm sure have been formally proven elsewhere. If the program had been written beginning with the proof and implemented the proofs of other concepts then the overall proof may have been much shorter.

Look, formal proofs aren't currently practical (and I doubt they will ever be) unless you're talking about extremely critical systems. They are expensive.

They aren't currently practical if you're writing them after the fact. They're practical if you're trying to advance the state of the art. They're practical if you want to write programs and proofs, 'hand in hand', and reduce the amount of defects as much as possible.

It's astounding that you call them expensive. TDD is pricey as hell. You have to write extra lines of code to test the lines of code in your main program. Not to mention the idea of running your tests every time you make a change. Not to mention continuous integration which requires setting up a server to run things (that's actual hardware which costs actual dollars). All of those things require time/money to set up and administrate. Adding more formality to your code only requires that you read and think.

thomasjeff · 12 days

Canadian news is like hyper-local news all the damn time. This is the kind of article that belongs in The Bumfuck-nowhere Times -_-'

Uberhipster · 12 days

Well I think we've seen how well the lack of correctness proofs is going from the millions of defects in our software and our willingness to ship products that are faulty.

Uberhipster · 13 days

What's wrong with his writing? No complaints about hoare or Wirth?

Uberhipster · 13 days

They focus on that because it's important. There's a lot of developers using open source software to create proprietary software. One day we'll get to the point where we can produce free software at our day jobs, but until then there's no sense in ignoring corporate networking and professional development.

Uberhipster · 13 days

Let's find em all and post them. The classics should be as widely available as possible.

PhonicUK · 17 days

I can't even watch this, it looks too much like Visual Basic and I can instantly see millions of lines of spaghetti copy/paste JavaScript code being written.

steeleduncan · 17 days

If you read about HaikuOS or BeOS they both prioritized UI responsiveness and the applications designed for them are typically multi-threaded which helps a lot in improving the UI latency.

Definitely needs to define/learn his terms better :S

chasejase · 18 days

Dude, start writing the script, this is the next Rome Sweet Rome!

maxwellhill · 18 days

Seriously dudes? Why not just make Freenet more user-friendly? The infrastructure is great, the user interface is not.

akshayk · 18 days

but I don't understand, why don't you just use grep and sed?! Surely those are enough! :P

Frankeh · 18 days

Oh, oops I forgot by Communism people mean state capitalism or totalitarianism. I meant communism as in socialism..

Frankeh · 20 days

Don't remember the decades of having a brutal right-wing dictator in power: check.

Frankeh · 20 days

Woah woah, communism doesn't "prey" on anything. Communism and socialism are a damn fine idea and their "preying" has given rise to the 8-hour work day, the living/minimum wage and other very important advances. Fascism only creates hate, dictatorship and authoritarianism.

Support the communists, socialists and anarchists and they'll fight back the fascists.

therealjimeh · 20 days

but they look shiny!

therealjimeh · 20 days

I had that problem; then I read the tutorial for info and you can access the quick documentation usually by doing: info -O whatever or info --usage whatever

If the nodes that provide a quick reference are consistently named you can do info --n Reference or whatever the node is called.

The halfway-to-tutorial verbosity in info pages actually annoys me.

I actually like that. Every program needs a quick reference, a tutorial and a manual. Info lets you combine that into one "book".

therealjimeh · 20 days

Or you could use Info pages which come with an interface much much nicer than less....

kjbekkelund · 20 days

Inevitably if there are asynchronous calls in play, you'll end up creating race conditions.

Only inevitable if you're slapping random code together, if you reason through it you should be able to avoid them? But that's fairly optimistic thinking, sorry :p

OMouse

TROPHY CASE

OMouse

TROPHY CASE

you'll need to login or register to do that

create a new account

login