aSanchezStern

9 ms·

31.
by aSanchezStern 2y ago
Not sure what the timeline on that is, but the University of Washington had housing specifically for PhD students with families in the 60s/70s IIRC
32.
by aSanchezStern 2y ago
Err, turning "shouldn't be talking to each other this much" to "shouldn't be talking to each other" is quite the leap. The author is clearly referring to the minute-by-minute stimulation that a microblogging pl
33.
by aSanchezStern 2y ago
Yeah, younger generations are spending less and less time with friends in person [1] and feeling lonelier and lonelier as a result [2]. [1] https://thehill.com/blogs/blog-briefing-room/4037619-teens-a... [2] http
34.
by aSanchezStern 2y ago
Location: Seattle, WA Remote: Yes Willing to relocate: No Technologies: C, C++, Python, Linux, Rust, PyTorch, Lisp, Formal Methods, HTML/CSS/JS. Resume/CV: https://www.alexsanchezstern.com/cv.pdf Email: alex.
35.
by aSanchezStern 2y ago
Uhh, endless recursion doesn't cause your typechecker to run indefinitely; all recursion is sort of "endless" from a type perspective, since the recursion only hits a base case based on values. The problem with non-well-found
36.
by aSanchezStern 2y ago
Err, only if humans have to be turing oracles to have that intuition, right? Plus, the halting problem only says that you can't have a procedure which will be 100% right on 100% of programs about whether or not they halt. Relax either
37.
by aSanchezStern 2y ago
The claim that "there can be no explainability of such models" is also completely unsupported. We know that some simple networks can be explained, and explanation is a human notion, not a formal one, so we can't know how much
38.
by aSanchezStern 2y ago
This is a particular philosophical conjecture, not a proven scientific fact. We don't understand enough about the human brain to prove whether it is fundamentally different from a very complex computer.
39.
by aSanchezStern 3y ago
Uhhhh, I'm pretty sure Lean already allows for formal verification of code. In the meta theory that tools like Lean and Coq operate, proofs and programs are very intertwined; it's not really possible to build a proving system in t
40.
by aSanchezStern 3y ago
Huh, good question. I think having a herbie-style error visualization graph built into an IDE would go a long way. In practice I think dynamic sampling is pretty good at capturing error behavior, and immediate visual feedback on the floatin
41.
by aSanchezStern 3y ago
It should be possible. Herbgrind is designed under the philosophy that it's not bad numerics themselves that are significant, it's how they affect the outputs of your program. So the reports are organized around program outputs (e
42.
by aSanchezStern 3y ago
I believe that's a PEBCAK error
43.
by aSanchezStern 3y ago
Wow, didn't expect this tool to be on Hacker News six years after publication! Herbgrind author here, ask me any questions you like! Also, if you're interested in this stuff, the Herbie project (which I also worked on) for numeric
44.
by aSanchezStern 3y ago
Sounds like you've stumbled into the wonderful world of machine-learning guided proof synthesis! While I don't think the full system you're describing has been built yet, many similar systems and pieces have. In terms of th
45.
by aSanchezStern 3y ago
Additionally, formal verification usability is an area of constant research, and the set of software for which it is the best ROI increases over time.
46.
by aSanchezStern 3y ago
1979 :) https://en.wikipedia.org/wiki/Logic_for_Computable_Functions
47.
by aSanchezStern 3y ago
Oh, I think you might misunderstand what I'm comparing it to. The other tools, like Proverbot9001, are exactly the NNUE scenario you describe, where a small neural network guides a search procedure to find proofs; they are more effecti
48.
by aSanchezStern 3y ago
Not directly, but COPRA which they compare to (and show about 3% more theorems proved than) is based on GPT-4 using an agent framework. And in the COPRA paper, they compare to using GPT-4 directly as a one-shot, and find it can only get 10%
49.
by aSanchezStern 3y ago
Note that this still doesn't seem as good at solving proofs as some of the specialized prover models at formal theorem proving that aren't LLM-based. In particular, they show a 3% increase in proves solved over COPRA on the MiniF2
50.
by aSanchezStern 3y ago
That... doesn't seem to check out. It can't be the going rate if it's infeasible. By definition the going rate is the rate that would allow you to afford doing the startup. Maybe you're comparing to the going rate of r
51.
by aSanchezStern 4y ago
Cool to see this new garbage collection work from OOPSLA 2023 coming up in blog posts! The blog post doesn't mention that this new algorithm looks like it's going to become the default in Firefox, and is being implemented in Chrom
52.
by aSanchezStern 4y ago
> which effectively means you work most of the year for the tax man and not yourself That would be true, if we lived in a world where your gross salary corresponded linearly to the amount of work you did. In that world, the hardest-wor
53.
by aSanchezStern 4y ago
I think if you could be a little more specific about what institutions think it's okay to discriminate against you in particular, it would really help.
54.
by aSanchezStern 4y ago
Hmm, but saying that you have privilege is not the same thing as saying you've done something wrong or are guilty, right? Even if you were born into an overall advantage, it wouldn't mean you had done anything wrong.
55.
by aSanchezStern 4y ago
Hmm, has anyone here met someone who espoused the argument "White people are inherently morally guilty due to racism"? I'm getting the sense that it might be mostly a strawman argument. Those I've actually talked to abou
56.
by aSanchezStern 5y ago
I believe you're basically referring to the computable reals; for the curious, here's the wikipedia page (kind of abstract): https://en.wikipedia.org/wiki/Computable_number and here's the paper where the
57.
by aSanchezStern 5y ago
This is actually fewer bits than they're using in the article, but that's not clear because they refer to their numbers by how many "[decimal] digits", not how many bits. The hardware doubles they're starting with a
58.
by aSanchezStern 5y ago
Unfortunately while Posits (and Unums) are more accurate for some computations, they are still designed around using small numbers of bits to represent numbers, so they have error in computations just like floating point. The argument for p
59.
by aSanchezStern 5y ago
For those curious, this tool uses arbitrary precision floating-point arithmetic (up to 3000 bits) to sample the input space and measure the error of different implementations of the function, then some clever numerical program synthesis to
60.
by aSanchezStern 5y ago
Yeah there are a few number systems that can do this kind of thing, ranging from rational implementations where the numerator and denominator are stored, all the way to the computable reals ( https://en.wikipedia.org/wiki&#x2

More ›