Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Hard Things in Computer Science

blog.frankel.ch

Post reply on HN
Print view View original

41–46 of 46 posts

Re: Hard Things in Computer Science

#41

Post by mbrodersen »

Beltiras wrote: post #21
deterministic wrote: post #5

Proving code correct is orders of magnitude harder than the rest IMHO. It is amazing that enough progress has been made that large scale projects like CompCert and seL4 can now be done successfully by small teams of people.

I'd say it is not hard but impossible. I have a hard enough time to get requirements specifications that are unambiguous. Proving I coded what I was asked for is not a rigorous science practice. It's a social contract.

No bugs have ever been found in CompCert and seL4. The NSA gave up trying to hack seL4. The first time that has ever happened. So yes there might in theory still be bugs in the specs for CompCert and seL4. However the results speak for themselves.

Re: Hard Things in Computer Science

#42

Post by mbrodersen »

Beltiras wrote: post #21
deterministic wrote: post #5

Proving code correct is orders of magnitude harder than the rest IMHO. It is amazing that enough progress has been made that large scale projects like CompCert and seL4 can now be done successfully by small teams of people.

I'd say it is not hard but impossible. I have a hard enough time to get requirements specifications that are unambiguous. Proving I coded what I was asked for is not a rigorous science practice. It's a social contract.

Non-proven correct software doesn’t even have formal specs. Having a formal spec is already light years ahead of other software because it forces you to nail down exactly what the code is supposed to do.

Re: Hard Things in Computer Science

#43

Post by llamajams »

Beltiras wrote: post #19
wiz21c wrote: post #11

Computing with limited numerical precision (aka floating point) is 1.000000000000003534 additional hard thing to deal with.

Modern computers can calculate with a very large finite precision using decimal types. We have so much machine to waste today that if calculations of that sort are relevant, just throw more iron at it.

Some of us have to write SW that can run on a potato.

Re: Hard Things in Computer Science

#44

Post by MaxBarraclough »

wiz21c wrote: post #23
Beltiras wrote: post #19

Earlier quoted context omitted.

Modern computers can calculate with a very large finite precision using decimal types. We have so much machine to waste today that if calculations of that sort are relevant, just throw more iron at it.

Nope! More precision sure helps but not in all cases. For example, having more precision will not help in boundary problems where you have to decide if something (for example an amount of money) is above or below a threshold. Moreover, many problems related to money) must compute with limited accuracy. For example, all intermediary results must be in 1/1000th of euros. You can use floats (yeah, I know, everybody say…

See also catastrophic cancellation, [0] although I'm unsure of the impact of using very large floating point types.

[0] https://en.wikipedia.org/wiki/Catastrophic_cancellation

Re: Hard Things in Computer Science

#45

Post by mbrodersen »

Mimmy wrote: post #10
deterministic wrote: post #5

Proving code correct is orders of magnitude harder than the rest IMHO. It is amazing that enough progress has been made that large scale projects like CompCert and seL4 can now be done successfully by small teams of people.

Interesting... I didn't realize there were large open projects that were formally verified. Are there other examples besides CompCert and seL4?

Formally Proven Binary Format Parsers:

https://www.microsoft.com/en-us/research/publication/hardeni...

Re: Hard Things in Computer Science

#46

Post by SOF3 »

Gordonjcp wrote: post #39

People say DNS is hard to get right but I don't see why. It's just cache invalidation and naming things, how hard can it be?

DNS isn't hard to get right. Using DNS practically is the thing that is hard. Is your cache something from NICs, ISPs, routers (and routers behind routers), operating systems (and operating systems behind operating systems), runtimes like containers (and runtimes inside runtimes), a Docker image that overrides /etc/resolve.conf, and then programming language (and if you're unlucky, a programming language that uses the stdlib of another language instead of the syscalls directly), third party libraries (and fourth party libraries used by third party libraries), or maybe yourself calling the wrong API. Or if you passed the domain name to a distributed system, the problem gets doubled because your distributed system may not share the same stack ... and then you figure out it's actually because the guy who said they updated the DNS record actually updated the A record without updating the AAA record.
Post reply on HN