Gajurgensen

6 ms·

1.
by Gajurgensen 2mo ago
I didn't mean to imply that the US is more likely than elsewhere to responsibly steer AI via policy. But I do think it is easier if it can be done internally as opposed to via international dealmaking.
2.
by Gajurgensen 2mo ago
It is incredibly important to whether the US can maintain its AI lead. If foreign competition is closing the gap only by distillation, then the frontier labs can focus on preventing distillation and maintain their lead that way. US dominanc
3.
by Gajurgensen 2mo ago
I'll note that not all segments of a proof are equally interesting. Many steps, perhaps even most when it comes to proofs about programs, are "obvious". I find that tactic-based proofs tend to be more legible than providing v
4.
by Gajurgensen 11mo ago
I was referring to issues that arise around the need for heterogeneous equality. As an example, consider the dependent vector type `Vec n`, which is an array of length `n`. An `append` function would have type `{n m: Nat} -> Vec n ->
5.
by Gajurgensen 11mo ago
I think the question of "necessity" is interesting, because between establishing that something is necessary vs the best option, I'd say the former is easier. And by agreeing that dependent types are not necessary (at least f
6.
by Gajurgensen 11mo ago
Very interesting. My takeaway is that Dr. Paulson's answer to the question is that there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary. I would have liked to read more about
7.
by Gajurgensen 1y ago
Think of higher level specifications which do not imply any details of the implementation. For instance, consider a sorting function. One could write a bubble sort and consider that a spec, but that is far too much detail, much of which you
8.
by Gajurgensen 1y ago
Program synthesis is of course very difficult in general, especially if you want it to be entirely automated. One option to make it more practical is to have the user drive synthesis from specification to implementation via something which
9.
by Gajurgensen 2y ago
Very interesting work! I'm curious how you handle loops/recursion? I imagine the `M` monad seen in the examples has a special primitive for loops?
10.
by Gajurgensen 3y ago
Theorem provers aren't just for mathematicians formalizing mathematics. Although, for that purpose, Lean seems to be very popular these days (perhaps followed by Coq?). Theorem provers are also used to formalize software and hardware s
11.
by Gajurgensen 3y ago
Coq is constructive be default, but you can add the axiom of choice and the law of the excluded middle to make it classical (other common axioms are functional extensionality, propositional extensionality, and proof irrelevance). Perhaps yo
12.
by Gajurgensen 3y ago
ACL2 has a documentation page for the theorems from this list proved: https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/in... A couple of theorems have actually been proved but not yet repor
13.
The Curry-Howard Correspondence(grant.jurgensen.dev)
3 points by Gajurgensen 5y ago|0 comments
14.
by Gajurgensen 6y ago
That's an awfully long-winded and confusing way to say you think "Boolean blindness" is too nitpicky. Personally, it seems like a pretty valid idea to keep in mind, especially as developers transition from a conventional impe
15.
by Gajurgensen 6y ago
The encoding of natural numbers in lambda calculus can be mysterious at first glance. I'm surprised the author didn't spend more time on it. No need to be so hostile about it though. Essentially, we represent numbers as functions
16.
by Gajurgensen 6y ago
Let's say getting those n and m values has a nasty type like `getNM :: IO (Maybe (Int, Int))`. All you need to do is map twice when using the original function. foo (n, m) = take n . filter p . drop m bar = fmap (fmap foo) getNM
17.
by Gajurgensen 7y ago
I highly recommend people interested in Coq start with Pierce's Logical Foundations. It is by far the most accessible introduction to Coq I've found. I'm working through Chlipala's books next. CPDT is a great deep-dive i
18.
by Gajurgensen 7y ago
I understand that the pervasive cynisicm can be exausting, but in the case of computer security, it really is warranted.
19.
by Gajurgensen 7y ago
It would be nice if there was a standard type alias for Either which explicitly labeled good/bad values. That being said, I don't think it takes that much energy to remember that the right is the good value. If you are comfortable
20.
by Gajurgensen 7y ago
This is great! It's not going to replace proof general + (evil mode) emacs for me, but this would be a great way to introduce people to Coq without worrying about installation.
21.
by Gajurgensen 7y ago
> Rust achieves impressive numbers with the most obvious approach. This is super cool. I feel that this behavior should be the goal for any language offering these kinds of higher order functions as part of the language or core library.
22.
by Gajurgensen 8y ago
This is pretty nitpicky, but I really dislike the postfix syntax for type constructor application.
23.
by Gajurgensen 8y ago
Why wouldn't it be a good solution to write something like Box, but with a new function that returns `Option<Box<T>>`? I'm not sure what Rust is lacking here.
24.
by Gajurgensen 8y ago
Learning about Church and Scott encoding was much more interesting than I thought it would be. I was expecting it to be tedious and banal, but I came out of it feeling like I had some sort of revelation. Imagining naturals, lists, trees, et
25.
by Gajurgensen 8y ago
If I recall correctly, most CakeML code is actually written in HOL4 and then translated down to CakeML, and compiled to machine code from there. Unfortunately there isn't very much in the way of documentation or examples for writing co