I made extensive use of Sage during a recent research project. The most useful thing about Sage for me is that it integrates cleanly many mathematical libraries, making it easy to export results from one tool into the…
Thanks for this, the reviews for this paper were very interesting. I do wish that they provided the meta-review, however, which summarizes the ultimate decision. Meta-reviews are written by area chairs, which are the…
I would like to point out before this discussion moves too far along that UCLA does in fact have an introductory programming course which is taught using Python: http://web.cs.ucla.edu/classes/enroll/97/ Students that…
Can someone with more knowledge than me contextualize this result? It appears to be making progress on the Riemann hypothesis, but why is this particular effort getting attention on HN?
While I agree that there are a lot of structural problems with universities and the way funding is allocated, I disagree with the premise that beginning with taxing graduate students is the correct way to do it.…
Rust macros are extremely impressive. This reminds me of Will Crichton's Lia library[0], which embeds a convenient matrix manipulation domain specific language inside of Rust. This seems like a very promising direction…
Alex Aiken has a very nice course: http://openclassroom.stanford.edu/MainFolder/CoursePage.php?...
His name is italicized because he is the primary author of OCaml (and a plethora of other great tools, like CompCert, the first fully-verified compiler). Overall, an exceedingly competent and productive programmer and…
One amusing thing about this epic tale is Serious Industrial OCaml User disregarded direct, relatively easy to implement, very sound advice from Xavier Leroy about how to debug their system! I would like to think that,…
> K-means is based on some quite wild assumptions - your data follows a specific case of the Gaussian distribution. Plus side is that the algorithm is relatively easy to understand and implement so it is a good starting…
You are right, perhaps my original post was unclear. The goal is to verify the transformation between LLVM and low-level assembly. I embellished slightly by equating the semantics of low-level assembly with CPU…
I think it's important to understand what's meant when someone says some piece of software is "verified". In this case, when they say LLVM is verified, they mean that they designed a formal correspondence between the…
There are a number of interesting examples in computer vision and psychology literature which document difficult cases for visual perception, see for example slides 14-19 in [0]. Ultimately, vision is a holistic process…
As a researcher that is currently working on implementing and improving existing PPLs, I'm very curious: what is your specific use-case that you have in mind for recursive queries?
My first thought is: Neat! Languages with different grammars, syntax, and libraries have different expressivities; my first thought is always compiler implementation in OCaml. I would love, for example, to…
One thing to consider is the possibility of your phone itself being compromised (stagefright et al.). Note how Duo issued a security advisory to limit access for Android devices [1]. A fully isolated component like a…
I'm personally shocked by how much power a DDoS has to potentially sway public opinion and influence the world at large. A few individuals have a hugely disproportionate voice in our public media by nature of the fact…
I made extensive use of Sage during a recent research project. The most useful thing about Sage for me is that it integrates cleanly many mathematical libraries, making it easy to export results from one tool into the…
Thanks for this, the reviews for this paper were very interesting. I do wish that they provided the meta-review, however, which summarizes the ultimate decision. Meta-reviews are written by area chairs, which are the…
I would like to point out before this discussion moves too far along that UCLA does in fact have an introductory programming course which is taught using Python: http://web.cs.ucla.edu/classes/enroll/97/ Students that…
Can someone with more knowledge than me contextualize this result? It appears to be making progress on the Riemann hypothesis, but why is this particular effort getting attention on HN?
While I agree that there are a lot of structural problems with universities and the way funding is allocated, I disagree with the premise that beginning with taxing graduate students is the correct way to do it.…
Rust macros are extremely impressive. This reminds me of Will Crichton's Lia library[0], which embeds a convenient matrix manipulation domain specific language inside of Rust. This seems like a very promising direction…
Alex Aiken has a very nice course: http://openclassroom.stanford.edu/MainFolder/CoursePage.php?...
His name is italicized because he is the primary author of OCaml (and a plethora of other great tools, like CompCert, the first fully-verified compiler). Overall, an exceedingly competent and productive programmer and…
One amusing thing about this epic tale is Serious Industrial OCaml User disregarded direct, relatively easy to implement, very sound advice from Xavier Leroy about how to debug their system! I would like to think that,…
> K-means is based on some quite wild assumptions - your data follows a specific case of the Gaussian distribution. Plus side is that the algorithm is relatively easy to understand and implement so it is a good starting…
You are right, perhaps my original post was unclear. The goal is to verify the transformation between LLVM and low-level assembly. I embellished slightly by equating the semantics of low-level assembly with CPU…
I think it's important to understand what's meant when someone says some piece of software is "verified". In this case, when they say LLVM is verified, they mean that they designed a formal correspondence between the…
There are a number of interesting examples in computer vision and psychology literature which document difficult cases for visual perception, see for example slides 14-19 in [0]. Ultimately, vision is a holistic process…
As a researcher that is currently working on implementing and improving existing PPLs, I'm very curious: what is your specific use-case that you have in mind for recursive queries?
My first thought is: Neat! Languages with different grammars, syntax, and libraries have different expressivities; my first thought is always compiler implementation in OCaml. I would love, for example, to…
One thing to consider is the possibility of your phone itself being compromised (stagefright et al.). Note how Duo issued a security advisory to limit access for Android devices [1]. A fully isolated component like a…
I'm personally shocked by how much power a DDoS has to potentially sway public opinion and influence the world at large. A few individuals have a hugely disproportionate voice in our public media by nature of the fact…