opus132

> in the same way that a C program linked against glibc is not a derivative work of glibc

I believe this is only as a result of the linking exception; I don't know if this has ever been tested, but my understanding was that linking (either statically or dynamically) against a library was generally considered enough to be a derivative work.

One example I'm aware of is Lawvere's fixed point theorem, of which Gödel's (first) incompleteness theorem, the undecidability of the Halting problem, and Cantor's theorem are all special cases.

Not really related to "group theory, linear algebra, real analysis, etc.", but interesting nevertheless.

It's quite a wide generalisation which really just captures the nature of diagonalisaion arguments, but it does formally tie together various proofs/theorems which "smell the same".

> Couldn't tell an average from a median

Without meaning to attack you personally (especially in the context of the rest of your comment), a comment like this annoys me a bit.

I presume by "average" you mean arithmetic mean, but the median is also an average, and depending on the context the median might be a far more useful statistic than the mean. Confusing the mean and the median is one thing, and perhaps you actually used this terminology in the interview; "confusing" "the average" and the median isn't really worthy of comment, and sounds more like a breakdown in communication between interviewer and candidate rather than a lack of technical knowledge. It just seems vaguely hypocritical to me to be expecting a certain level of ability from the candidate and then using imprecise/informal terminology.

The "obvious solution" would surely be for grsecurity's customers to band together into a cartel to put an end to this pretty unpleasant behaviour?

This seems pretty good from a brief flick through; the author. Graham Hutton, is pretty well known in the CS community.

Some other resources for people who find that this piques their interest and that they want to go deeper:

* Formal Reasoning About Programs ("FRAP") by Adam Chlipala - available for free here: http://adam.chlipala.net/frap/. Forms the basis for 6.822 at MIT, and comes with an accompanying Coq formalisation (as well as psets in Coq).

* The Formal Semantics of Programming Languages: An Introduction by Glynn Winskel.

Undergraduate studies in the US in general are very different from in Europe.

I did my undergrad (EECS) at Imperial and MIT (for my final year), and the difference between the two was pretty enormous. My home department expected me to take five graduate classes (plus some undergraduate classes for "light relief") over the course of my year at MIT, something the other undergraduates there thought was very unusual.

In general US undergrad is much broader than in Europe, and doesn't go into as much depth, even though a US bachelors is a year longer than a European one. Not necessarily a bad thing, it just depends on what you consider the point of an undergraduate education to be; I'd say that most European universities try to structure degree programs which can funnel you straight into research or industry without having a sudden step up (the step up from undergrad to graduate studies in the US is pretty huge) whereas the US thinks it's more important to develop yourself in a broader range of areas rather than see the degree solely as a means to an end.

They both have strengths and weaknesses (having experienced both) and I don't think either can be said to be better.

This looks more like someone proved some trivial lemmas about lists and wrote the simplest possible DSL to do some list manipulations rather than anything close to resembling a serious piece of work on formally verified text editors.

This is first-lecture-learning-Coq level stuff to be completely honest; it's interesting if you've never seen Coq before, but it's not really what it claims to be at all. The amount of work to go from this to "formalizing full-nlown text editors, such as vim" is enormous.

If we remove the proof scripts (and duplicated statements of Lemmas/Theorems in Gallina and mathematical notation) since these would never be included in a published paper (only as an accompanying artefact unless a novel tactic/proof scripting method is the actual topic of the paper), the length of the paper almost halves and the amount of substance becomes clearer.

Nigel Smart's Cryptography Made Simple is a great book which covers elliptic curve cryptography amougst many other topics; despite its name it's a very technical book, but it's easily accessible to anyone with a CS/EE/Maths/Physics degree.

You can grab a copy from SpringerLink for free at the moment here: https://link.springer.com/book/10.1007%2F978-3-319-21936-3

In addition to the other reasons already mentioned, this would likely reveal a lot of small details about the underlying microarchitecture of the FPGA fabric which is a (highly valuable) trade secret.

You mean a piecewise definition of a function? I don't think this is unidiomatic or discouraged in Haskell at all.