September 28, 2016

Questions for Tech People

I saw this on Instapundit and immediately thought of the Battle of Midway, the Verona transcripts and Bletchley Park.

The language follows step-by-step, logically, and can be tested just like a mathematical proof. So why is this formal verification essentially hack-proof? Because most hacks are made by exploiting bugs and errors in code. Code that’s gone through this process, with this approach, is supposed to be bug-proof. So there are no holes for hackers to exploit, because the code just works.  
Emphasis mine.

In your professional opinion, how applicable (as a practical matter) would this be to the IT industry in general?
Do any of the IT people reading this blog think that the "Internet of Things" is a cracking good idea which will provide benefits far surpassing its potential security risks and bot-farm potential?
Would it be a good idea or a waste of time to make a class or 2 in code mandatory in highschool? If so what language would you reccomend? Does it matter that much? 
Turning over the internet to ICANN: discuss. 

Why is Minx not listed here?

Posted by: The Brickmuppet at 05:29 PM | Comments (5) | Add Comment
Post contains 190 words, total size 2 kb.

1 I'm not a fan of formal verification. It was around as long as the idea of Tokamak was. And... Same result. A interesting demos, nothing practical. Meanwhile the computing has developed enormously. Frankly at this point I'm beginning to suspect that verification is a snake oil.

Posted by: Pete Zaitcev at Wed Sep 28 19:26:51 2016 (XOPVE)

2 In order:
1) Formal verification doesn't scale well, and to do it properly, you'd have to start at the firmware level for each piece of hardware in your system, and work your way up through the device drivers, operating system, compilers, and libraries. By the time you finished vetting a machine to run your "hack-proof" code on, all the parts would be obsolete. 
2) Most Things should only be on a local or personal area network, and have no direct access to the Internet. NAT's a good model, despite all the IPv6 weenies trying to assign a unique global address to your toaster and fridge. Remote access to your Things should not be through a cloud service, but through an encrypted channel to your gateway device. Also, don't buy Things from a company that doesn't have a good track record for long-term security update support (which today pretty much means "don't buy Things").
3) Waste of time. Give them classes in statistics, critical thinking, and discrete math instead, and they can apply those skills anywhere, including learning to code in whatever language is trendy this week. As a bonus, they'd be resistant to scams and most political arguments.
4) The people who want control over the Internet want control over how people use it, so "no".

Posted by: J Greely at Wed Sep 28 20:05:09 2016 (CLiR9)


Fads in computer science come and go. "Proving code" has been around for a hell of a long time, but as J says, the problem with it is that it's too expensive and it doesn't scale well.

It takes an absurd amount of time and a huge staff. And the cost and time grow faster than 1:1 as the project size increases.

The best crafted software I know of was the operating code for the Shuttle onboard computer. The system had five CPUs, four of which came from one company and the fifth from another. They were independent designs.

The code that ran on them was written twice, once for each architecture. And the system was constantly self-checking, not just that all five computers agreed and got the same answer but also that they got it at the same time. Just an amazing system.

And the very first test launch of the shuttle, with two test pilots on board, was scrubbed at the last minute because of a computer problem. The one computer decided that the four computers were taking too long and it hit the stop button. (Of course, it wouldn't have done that if they were already flying, but before launch it was the right response.)

It turned out the one computer was right, too. The software for the four computers had to be rewritten.

Any experienced programmer knows that "bug-free code" is a phantasm. It's long been a truism that if your code has no bugs, it's because it's trivial. Any non-trivial sofware will eventually fail.

Posted by: Steven Den Beste at Wed Sep 28 20:38:07 2016 (+rSRq)

4 As Donald Knuth once wrote: "Beware of bugs in the above code.  I have only proved it to be correct, not tested it."

Posted by: Pixy Misa at Wed Sep 28 21:52:34 2016 (PiXy!)

5 I think there's room for... not the Internet of Things as it's currently envisioned (I don't need my fridge ordering groceries), but a more distributed computer system.

Right now I do just about all my computing sitting at my computer. That's mostly because a lot of it is gaming, and well, a tower is the only thing that can run this stuff at 4K. But a lot of the simpler stuff, especially a lot of the communication stuff, could be distributed throughout the apartment without too much trouble. The only real problem is figuring out what kind of displays, etc., would do the job most easily... and the fact that a lot of the software is assuming "you're using only one device right now and that's this one." Even if I had a tablet in every room, most of the chat stuff would interpret each one as a separate login and kick the rest off, so I couldn't just go from room to room and continue a conversation without a lot of logging in and out, etc.

There's also the question of utility. How much would that really be worth to me? What's the added advantage of that kind of setup versus "main desktop, and a tablet or laptop you can use elsewhere"?

Forget teaching coding in high school. We'd do better to teach personal finance (though that would lead to a lot of awkward questions... "Hey, teacher, all the example problems in the book for the benefits of compound interest mention people getting 5% on their savings account, but all the ones they actually offer give .5% instead...")

If we do turn over authority to ICANN, we'd better do so with the proviso "but if you piss us off, we will just take it right back." ;p

Posted by: Avatar_exADV at Thu Sep 29 14:15:26 2016 (v29Tn)

Hide Comments | Add Comment

What colour is a green orange?

31kb generated in CPU 0.02, elapsed 0.1189 seconds.
68 queries taking 0.104 seconds, 264 records returned.
Powered by Minx 1.1.6c-pink.