mauricioc

11 ms·

61.
by mauricioc 6y ago
There is no such thing as a "linear value" per se, since linearity is on the arrow. But speaking of linear values makes sense when there's an ambient monad, and all of the restrictions you expect are enforced; see Section 2.7
62.
by mauricioc 6y ago
Exactly. Even if one doesn't know of him beforehand, this can be inferred from context: the emcee/herald refers to him as just "andy", suggesting he is a known figure in the context of the conference. A quick search for
63.
Lean Together 2021 – A meeting for Lean users and other formalizers(leanprover-community.github.io)
2 points by mauricioc 6y ago|0 comments
64.
by mauricioc 6y ago
Probably a coincidence, but also Lean Together 2021 [0] is happening next week and it is likely that many Lean 4 details will be revealed there. [0] https://leanprover-community.github.io/lt2021/
65.
by mauricioc 7y ago
Sure, using a denominator of 10^n gives 1/10^n precision, which is pretty good. And this is fine for applications! However, defining goodness in terms of absolute error makes the resulting problem of "how good an approximation can
66.
by mauricioc 7y ago
https://dblohm7.ca/blog/2015/07/28/interesting-win32-apis/ notes that Windows has the required APIs, and that Firefox already supports handling memory pressure notifications on non-Windows platforms
67.
Web Replay (Formerly Known as Firefox Replay)(webreplay.io)
7 points by mauricioc 7y ago|2 comments
68.
by mauricioc 7y ago
Title slightly editorialized because the name "Firefox Replay" showed up in previous HN discussion at https://news.ycombinator.com/item?id=21655958 (1596 points)
69.
Remove Firefox Replay(bugzilla.mozilla.org)
3 points by mauricioc 7y ago|2 comments
70.
Knuth's 25th Christmas Lecture – Pi and the Art of Computer Programming [video](youtube.com)
2 points by mauricioc 7y ago|0 comments
71.
by mauricioc 7y ago
The theorem you quoted is Van der Waerden's theorem [0], not Szemerédi's. It is significantly easier to prove than Szemerédi's result. The article correctly states Szemerédi's theorem, if you interpret "sufficiently
72.
by mauricioc 7y ago
Compiler bugs are not what I had in mind, so this answer is very reassuring! The original thread led me to believe this was not an absolute, official policy of the Rust project, but I am happy to hear it is.
73.
by mauricioc 7y ago
Totally reasonable stance, in my opinion, since Rust moves quickly and formalizing things takes time. But what is the stance on soundness bugs? Are they sometimes acceptable as permanent parts of the language, or is it a goal to eventually
74.
by mauricioc 7y ago
Simon Peyton Jones initial intuition [0] was that Rust would be full of soundness holes due to not starting with a full formalization. Derek Dryer, Ralf Jung and others in the RustBelt project [1] did amazing work in formalizing Rust's
75.
by mauricioc 7y ago
She has a list at https://twitter.com/natashenka/status/1155940732084973568 (recall that "remote, interaction-less" means "do not require any physical interaction from the target to be exploited, an
76.
by mauricioc 7y ago
The line can be blurry sometimes, but it's roughly the difference between research and teaching. MathOverflow is meant to help mathematics researchers. At its best, it's like being able to walk over to a colleague's room in a
77.
Telegram rolls out fix for voicemail hack used against Brazilian politicians(zdnet.com)
1 points by mauricioc 7y ago|0 comments
78.
by mauricioc 7y ago
It only reduces the odds to such a tiny number if your password is in the list (otherwise, guessing the remaining 136 bits of the hash is infeasible). If that's the case, however, sending a part of the hash to the server is still the b
79.
Brouwer–Heyting–Kolmogorov Interpretation(en.wikipedia.org)
2 points by mauricioc 7y ago|0 comments
80.
by mauricioc 7y ago
One exciting new development is "Cubical Type Theory: a constructive interpretation of the univalence axiom" [0], a constructive version of homotopy type theory. The "axiom of choice" in this context is not really an axi
81.
Survey: Autopilot name causes people to overestimate Tesla capabilities(arstechnica.com)
2 points by mauricioc 7y ago|0 comments
82.
Agda-sessions: Learn the Agda basics in three 2-hour sessions(github.com)
3 points by mauricioc 7y ago|0 comments
83.
Security Advisory for the Standard Library(blog.rust-lang.org)
54 points by mauricioc 7y ago|6 comments
84.
by mauricioc 8y ago
Related: http://www.wonder-tonic.com/geocitiesizer/
85.
Am I the only one seeing the '90s retro theme, with the unicorns and sparkles?(meta.stackoverflow.com)
68 points by mauricioc 8y ago|23 comments
86.
by mauricioc 8y ago
Portuguese-origin names can be a bit ridiculous in this sense as well. Famously around here, the first emperor of Brazil was named "Pedro de Alcântara Francisco António João Carlos Xavier de Paula Miguel Rafael Joaquim José Gonzaga Pas
87.
by mauricioc 8y ago
Are you utopcell@google.com as in [1]? If so, I would say that's worth mentioning. [1] https://research.yahoo.com/mobstor/publication_attachments/w...
88.
by mauricioc 8y ago
According to Donald Knuth, "This algorithm goes back to Nārāyaṇa Paṇḍita in 14th-century India; it also appeared in C. F. Hindenburg's preface to _Specimen Analyticum de Lineis Curvis Secundi Ordinis_ by C. F. Rudiger (Leipzig: 17
89.
by mauricioc 8y ago
I feel like I should point out this 20+kLOC project is the work of just one engineer (Brian Hackett), although of course several people helped with reviews and feedback. It's very impressive and inspiring work. Major props!
90.
by mauricioc 9y ago
The presentation addresses this in a way. The argument is that in Coq you can write proof _scripts_ ("repeat this simplification operation until it does nothing", "pattern match on this definition and apply this operation to

More ›