Live data from Hacker News

Hard Things in Computer Science

blog.frankel.ch

31–40 of 46 posts

Re: Hard Things in Computer Science

#31

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.

That's a software engineering problem, not a computer science one.

Re: Hard Things in Computer Science

#32
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.

As someone who worked on indoor positioning at Apple, I’ll disagree with this. We were doing some basic probability estimation of WiFi signals (ML techniques but not AI). First, you still need the computation to compute within a reasonable time/power envelope. Secondly you need it to be numerically stable (adding a large number of very large and very small floating point together). Doing this using infinite precision libraries would be infeasible because while fast they aren’t as fast as regular floating point. Additionally using regular floating point meant that we could utilize BLAS and Lapack which had SIMD HW acceleration. At the end we managed to fit this within the power envelope of GPS with minimal CPU utilization (after many rounds of optimizing the CPU and WiFi scanning). Additionally, the runtime performance of the core numerical algorithm determined how long the training (building the maps was similar to locating yourself) and -validation tools (checking if a commit changed runtime performance) ran.

Now sometimes you don’t need this level of effort but don’t underestimate just how much CPU you might be leaving on the floor. Sometimes it can mean what seems like an impractically slow algorithm actually runs fine. Even if you ran an infinite precision version of the ML code on a modern desktop CPU you might struggle to get perf to get the system to run in real-time (we needed to run the simulation within 5-10 ms and then do a bunch of even more complicated math to compute the blue dot location every 250ms)

Re: Hard Things in Computer Science

#33
post #9

Earlier quoted context omitted.

Yeah I stopped reading at that point, cache invalidation is not 'also known as TTL'.

It's a simplification but it isn't wrong. Mostly.

Write through cache doesn’t need invalidation. You can also invalidate through cache shoot downs. I’m sure there are many other techniques. Invalidation just means “what’s your strategy for removing things from the cache”. Using an expiry age is only one technique.

Re: Hard Things in Computer Science

#34
Not to diminish how hard these things can be. It just reads more like a "hard things in (somewhat advanced) software engineering" more than computer science IMO. I expected reading things like "is graph isomorphism NP-complete?" at least included.

Re: Hard Things in Computer Science

#35

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.

I agree with "impossible". In fact, it's worse than you say. Specs can be unambiguous and still be wrong. How do you prove that the specification doesn't have a bug?

And then, you can formally prove that code does not have certain kinds of bugs. You cannot formally prove that code has no bugs, because 1) you don't even know all possible kinds of bugs, and 2) even for the kinds you do know, you don't have formal proofs for all of them.

Re: Hard Things in Computer Science

#36

Earlier quoted context omitted.

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.

I agree with "impossible". In fact, it's worse than you say. Specs can be unambiguous and still be wrong. How do you prove that the specification doesn't have a bug? And then, you can formally prove that code does not have certain kinds of bugs. You cannot formally prove that code has no bugs, because 1) you don't even know all possible kinds of bugs, and 2) even for the kinds you do know, you don't have formal proof…

Bugs in the specs. Yum.

Re: Hard Things in Computer Science

#37
I would add “synchronization of any kind”. Anything from versioning/code collaboration to syncing any kind of state between separate systems. I have worked with a lot of (mostly inexperienced) engineers who underestimated just how complex something like Git can be and the incredible amount of engineering behind it.

Re: Hard Things in Computer Science

#40

As another problem of applied CS I also suggest to add "Character Encoding" to the list of strongly underestimated complex problems :)

Agreed, and also just text in general, internationalization, line-breaks, horizontal vs vertical text, left-right vs right-left, etc, etc. OTOH that starts getting quite "application oriented" and where do you draw the line? compsci is perhaps more about computation and how to achieve it, analyze it, etc, and in that case even dates and times should not be in the list, being an "application" domain concern.

Related:

Text Rendering Hates You - https://news.ycombinator.com/item?id=21105625 - Sept 2019 (170 comments)

Post reply on HN