> 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".
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.
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.
Or they could pay the ransom, which they deem to be less expensive than dealing with the regulator, and improve their data security to ensure they don't get caught out again.
I fully understand (and support) the reasoning behind GDPR; I just think that in this case there is a path which is easily open to abuse by attackers.
No I can't, and I don't see how anyone would know of such an example unless they were directly involved; if such occurrences were known publicly, the regulator would also know, which defeats the entire point.
I don't have any idea regarding the scale of the impact laws like GDPR have had on cybercrime; I'm just pointing out that there's clearly an interaction (and I'm not the first person to say this by any means), and that I would be interested to know whether the California privacy laws had any impact on UC's decision.
I'm a big supporter of GDPR by the way; this isn't an "anti-GDPR fantasy", just my observation on a potential interaction between GDPR and cyber crime.
Within the EU, GDPR seems to have an interesting impact on how companies/organisations respond to cyber attacks like this: if they don't pay the ransom, the data is leaked, and they are now liable under GDPR and will likely have to pay a (very large) fine to the regulator for the data leak. Attackers are surely savvy to this, and should set the ransom to be slightly lower than what they estimate the fine would be, which 'motivates' the organisation to pay the ransom.
In theory however, even if the organisation recovers the data by paying the ransom, they should still report this as a data breach, and would probably be fined by the regulator even though the data was recovered, since the breach still occurred in the first place.
I'd be very interested to know the impact the new California state laws on privacy have had on UC's decision to (seemingly) pay the ransom; I'm not based in the US, nor am I familiar with the jurisdiction, but I imagine that this will have been taken into account and might explain why UC acted differently to MSU here.
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.
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.
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.