Viewing profile — derrak

In case you’re not familiar, I will point you to the classical program synthesis literature. There the task is to take a spec written in say first-order logic, and output a program…

Wow! I really enjoyed this. The 2.5D rendering gives a lot of opportunities to visually obscure the insight that’s necessary to solve the maze. It makes me think that a good maze s…

Makes me think of academic papers that overhype their contribution. Also makes me think about AI hype.

How do you define determinism?

Lets solidify definitions. A procedure is deterministic iff for all inputs, it always produces the same output on that input. Now, I am going to be pedantic because words matter he…

This app runs contrary to one of the most prolific stop smoking guides. https://www.allencarr.com/easyway-stop-smoking/top-tips-to-s... > You’re going to stop naturally so carry on…

> As a countermeasure to key disclosure laws, some personal privacy products such as BestCrypt, FreeOTFE, and TrueCrypt have begun incorporating deniable encryption technology, whi…

I like. On the issue of “are LLMs good at lisp” I have a bit of a tangential response/observation. I saw this [paper]( https://ai.meta.com/research/publications/logic-py-bridging-.…

> I also thought about pushing more toward Lean and theorem proving instead of a lighter SMT-style direction I think your intuition here is good. For these settings I think you wan…

Happy to help. In general, I think counterexample generation is more important than proofs when it comes to software (most of our software is “trivially” wrong). The world might no…

This looks very interesting. I think the translation from L0 to L1 is going to become more and more important. There have been a lot of discussions here on HN about how natural lan…

I do use ACL2, although I don’t do many proofs. When I do, the proofs usually go through automatically or require me to state only a few lemmas or tell the tool how to do the induc…

Noted, thanks. I don’t know what non-computational intelligence would look like but I guess I’ll keep my mind open.

> The proofs stop at the language boundary. The bugs don’t. In formal verification, you have to model everything you care about. I suspect we’ll see large fragments of popular lang…

Looks interesting. Anything in particular from it that you think relates to my comment?

> Certainly it is much closer to a brick than to a human. I disagree with this premise. A computer approximates a Turing Machine, which puts it far above a brick.

> Recently I’ve been thinking about coding with AI in terms of it being a process of navigating a tree of probabilistic outcomes. I think this is the correct way to think about aut…

We can keep our discussion about church turing here if you want. I will argue that the following capacities: 1. creating rules and 2. deciding to follow rules (or not) are themselv…

As long as agnosticism is the attitude, that’s fine. But we shouldn’t let mythology about human intelligence/computational capacity stop us from making progress toward that end. > …

Note that I prefaced my comment by saying the parent might be right about LLMs. > That's irrelevant. My comment was relevant, if a bit tangential. Edit: I also want to say that our…

The Church-Turing thesis comes to mind. It would at least suggest that humans aren’t capable of doing anything computationally beyond what can be instantiated in software and hardw…

> non-deterministic printer. I interpret non-deterministic here as “an LLM will not produce the same output on the same input.” This is a) not true and b) not actually a problem. a…

Maybe you’re right about modern LLMs. But you seem to be making an unstated assumption: “there is something special about humans that allow them to create new things and computers …

First, I have some advice if you are open to it. Apply a spell/grammar checker to your post before sharing it with other people. Your post has several typos and many people will st…

> AI must control the proof search, not delegate to a black box. Cannot disagree more. Take a look at modern SAT solvers, SMT solvers, and automated theorem provers like ACL2. We s…