So called "safe languages" are shit because they are slower than C, so you end up giving away performance. How to avoid this performance-security trade off?
Follow seL4's example. Verify the software through formal mathematical proof using a theorem prover (such as Agda, Coq, Isabelle, etc.). This will assure that the specification of a piece of software has certain properties and, then, that a design (in C) implements a specification correctly. In recent years, it has become possible to apply formal verification directly to the code that implements the software and to show that this code has specific properties.
In other words, you get a C program (high-performance) that is mathematically shown to have no buffer overflows, null pointer exceptions, use-after-free, or anything else you designed in the theorem prover.
Name:
Anonymous2014-12-30 15:22
Nope, C is useless unverifiable shit. To be able to verify it, you have to use a restricted subset of C. Also writing up a proof of imperative shit is very hard and time-consuming.
>>3 If C could be formally verified, Hongwei Xi wouldn't need to invent a whole new language, ATS, just to eliminate runtime array bounds checks from C.
Name:
Anonymous2014-12-30 17:06
>>8 I agree, on that basis ATS was an unnecessary invention.
It is also the only evolving formally-verified code base of the order of 10 000 lines of code and we report on maintaining it for almost a decade together with its now 480 000 lines of Isabelle proofs and specifications.
See, I told you that verifying C diarrhea is a pain in the ass. The proofs and specifications are 480 times larger than the C shitcode itself! And they probably only prove only the primitive propositions, not algorithm correctness.
Name:
Anonymous2014-12-30 17:46
Also 10,000 lines of C code aren't big enough to be an OS. BSD has 8 million, Linux has 15 million, and Hawking knows how many lines Windows has. So what they claim to have verified is not a general-purpose kernel.
Name:
Anonymous2014-12-30 19:44
>>8 He created ATS just so it was easier for programmers, but it loses performance.
The human resources required for even a relatively small-scale verification are tremendous, as shown by seL4
The seL4 project is based on the family of micro-kernels known as L4 [18]. Recently, a refinement proof was completed [16] that demonstrated the adherence of a high-performance C implementation to a generated executable specification, created from a Haskell prototype, and checked in the Isabelle [21] proof assistant. The Haskell prototype is itself checked against a high-level design. One weakness is that changes made at a high-level can have rippling effects and may require the entire proof to be redone.
If the software you are writing is huge, you have really limited resources and performance isn't an issue, then languages such as ATS may do the job for you. But there's nothing better than proven-secure C. High-performance and safety. The only trade-off: time spent on the project.
Name:
Anonymous2014-12-30 19:46
lol all these stupid 20 year olds who the fuck do you think you are, kids? get back to your undergrad class
Name:
Anonymous2014-12-30 19:46
>>11 Microkernels are much smaller than monolithic kernels, idiot. MINIX 3 has about 6,000 lines of executable kernel code.
Name:
Anonymous2014-12-30 19:47
Also 10,000 lines of C code aren't big enough to be an OS
I wrote a megalithic kernel in 738329775459637 lines of code.
Name:
Anonymous2014-12-30 23:51
>>16 Your kernel doesn't have a full set of hardware drivers like what you get in Linux or any kBSD. That's where most of the code weight goes to in a full featured monolithic kernel.
Well there you go, as we all know, all programmers have all the time we need to formally prove C code because the binary code is faster oh wait... no, we don't have all that time. We use safe languages because programmer time is more expensive than computer time, it's quicker to deliver software using safe languages. We will use C when it's obvious that we need a strict account for the computer resources we need. The vast majority of application programming on high-powered general-purpose computers do not have such a requirement.
Your body doesn't have AIDS like mine. That's where most of the cell weight goes to in a full featured human body
Name:
Anonymous2014-12-31 0:11
>>21 lol, this is why corporations (capitalism) is harmful to computing progress. Computing (programming a sub-set of) is a communist, military, and individual genius sort of thing.
get fucked retard ahhahahahhahaha, if you cant outdo your computer at arithmetic (in your head of course) then you shouldn't be using it in the first place kiddo
This will assure that the specification of a piece of software has certain properties and, then, that a design (in C) implements a specification correctly.
And how do you prove that the specification is correct, or that the "certain properties" are what you want anyway? What, or who, defines those? Are the requirements correct or wanted? Does this software do what the users really want? Does it not oppress the users? ...? ...? What is the meaning of life?
At some point humans have to make the decisions, not the machines, and there are always going to be idiots to screw things up no matter what, so why don't we stop creating more abstract bullshite that just takes freedom and responsibility away from humans and encourages them to be even more stupid, teach people to think correctly, and take the idiots out back to be shot!
At some point humans have to make the decisions, not the machines, and there are always going to be idiots to screw things up no matter what
Yes but programming with proofs is an excellent way to improve correctness through redundancy. First you tell the computer what your algorithm is supposed to do, then you actually code the algorithm. Knowing the intension behind your code, the compiler can double-check it and tell you if what you wrote is not exactly what you wanted. Without that proof-of-intension, the compiler has no idea what you're trying to do and so will blindly execute every instruction no matter how erroneous it is.
Name:
Anonymous2015-01-01 11:41
Last time I already tried to prove PHP can do anything when it comes to network protocols by implementing a DNS server. This time I’m doing it again with a server-side implementation of the SSH2 protocol.
You probably know SSH at least by its name. It’s a of secure telnet replacement which also allows many other things such as port forwarding, remote file management (with sftp) and more.
With PHP I could write a fully working SSH server in only 3 days.
and tell you if what you wrote is not exactly what you wanted
That doesn't stop you from writing something that you wanted at first, but changed your mind later, etc.
"Are you sure? Are you REALLY sure? Are you sure that you're sure? Are you sure that you're sure that you're sure?" There's no end to this madness.
Name:
Anonymous2015-01-01 16:29
>>39 Yes, programming with proofs is brittle, and not good for changing design goals. And also not 100%-proof. But it still offers more assurance than unproven code. Like, if you prove that your sorting algorithm really sorts, then it will actually and honestly sort.
Name:
Anonymous2015-01-03 2:48
Someone should write a program that can check any arbitrary program to make sure that it is correct.
Name:
Anonymous2015-01-03 12:39
Someone should write a program that can check any arbitrary anus to make sure it is anus.
>>44 You are confused. I hope that doesn't happen often when Ted Nugent is involved, but back to the topic at hand. The "manliness" code test is Knuth's “Man or Boy Test”—http://rosettacode.org/wiki/Man_or_boy_test
Actually, I would like to see the Symta solution to this problem.