sangel

Joined 10 years ago

Karma
140
Submissions
24
Member since
Nov 30
CS Prof at UPenn
View on Hacker News

Recent submissions

Comment · 5 months ago
This is the entire formal verification effort, as far as I can tell: https://codeberg.org/gregburd/aether/src/branch/main/aether/...

They use TLA+ with TLC which model checks the write ahead log (a component of the system). But that only models the WAL protocol, not the actual Rust code and not the other 99% of the system.

Any formal verification is of course awesome to see though.

Comment · 1 year ago
My totally uneducated guess is that they leak exaggerated numbers on purpose to make the real numbers look less bad in comparison. The idea being that a few days before the official news everyone is talking about a potential 30 or 40K people layoff. Then, when the official news come out and state that they are laying off 14K people, it sounds less dramatic (in relative terms). This makes people (who are not affected by this) to feel like the news were overblown and are not as significant.
Comment · 1 year ago
Obviously not. Suppose the input to my function is a 64-bit integer. My test cannot possibly try every possible 64-bit integer. It would take years for such a test to finish.

This is why tools like formal verification and symbolic analyses can help you establish that for all possible integers X, your function does the right thing (for some definition of “right”). You get this assurance without having to actually enumerate all X.

Comment · 3 years ago
Very inefficient. Like wildly so. Specifically if you have a very small database and you preprocess it with their techniques, the resulting database is petabytes in size. But the results are very beautiful.

There are no obvious ways to improve on this work, so it is not a matter of engineering. We really do need another breakthrough result to get us closer to practicality.

Comment · 3 years ago
At least in my department, this will not work as long as the applicant's supervisor or dissertation committee members are still in the department. The crux of the issue, in my mind, is that it is hard to have candid and unbiased discussion about a candidate when the supervisor / dissertation committee is part of that discussion.
Comment · 3 years ago
This is strange to me. Many universities, including mine, avoid interviewing applicants with a PhD or postdoc from the same institution to which they are applying.
Comment · 4 years ago
This is basically what we did in our project: https://www.cis.upenn.edu/~sga001/papers/pung-osdi16.pdf.

We never built it into a product because we couldn't figure out a way to monetize it to pay for the servers.

Comment · 4 years ago
From my experience your first number is off by 3X and sometimes more depending on the university.

But yes, you make less as a professor than you do in industry.

Comment · 4 years ago
Comment · 4 years ago
High risk compared to what? The alternative is absolutely no privacy (status quo) or no/limited functionality (not very useful). Seems like strictly better than having no privacy.
Comment · 4 years ago
You can formally verify all the way to C, C#, Haskell, or even assembly if you use tools like Dafny, Coq, or Vale (for verified assembly). Several projects do this. It’s a lot of work for sure though.
Comment · 4 years ago
Non interactive zero knowledge allows one proof to be checked by many verifiers. I think folks would still consider that to be a zero knowledge proof no?

That said, yeah this hashing example is not zero knowledge because, among other things, the hash is not hiding.

Comment · 4 years ago
This hasn’t really been my experience at all. I find students at my university (an ivy) to be pretty reasonable and only complain if there is a mistake during grading. In that case they are absolutely entitled to do so. They also seem to really enjoy challenging classes.
Comment · 4 years ago
It is 40 degrees F right now… in mid May. And has been all month and basically all year since last November.

I don’t see how you can call that good temperature.

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton