Viewing profile — Gajurgensen

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 inte…

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 preventin…

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 pr…

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 `app…

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 …

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 ar…

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 tha…

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 synthes…

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?

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 pro…

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, prop…

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…

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 d…

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 thoug…

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…

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…

I understand that the pervasive cynisicm can be exausting, but in the case of computer security, it really is warranted.

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 t…

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.

> 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 …

This is pretty nitpicky, but I really dislike the postfix syntax for type constructor application.

Why wouldn't it be a good solution to write something like Box, but with a new function that returns `Option >`? I'm not sure what Rust is lacking here.

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 s…

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…