Also check out Morph Labs, which is working with Lean to create an AI proof assistant. Cool startup by ex-OpenAI folks.
Essentially a strong type system of Lean can help with constrained generation. Thus every token would always lead to some valid (if not correct) proof in Lean, iiuc. Maybe people @ Morph can comment.
Oh, this is great. This article and conversation with Marcelle led me down a rabbit hole of Prolog, Minikanren, and Reasoned Schemer.
Not quite out yet.
I am thinking about using this idea of Prolog as AST to build an ai-first, reactive IDE. DM me at @eating_entropy on Twitter or email me at [email protected] if you are interested.
Hey! I noticed you in a comment about cold calling. I have been doing something similar (near 100 in the past month), and am at a dilemma regarding how to approach it. I am curious if you are still cold calling.
Really good stuff, but some minor things: your url doesn't work; went to your twitter profile, and it seems you meant https://chatcraft.org? Also, you are un-dm-able on twitter. (I am @eating_entropy if you want to talk more)
The interactivity is one. It's easy to evaluate expressions from within the editor. I am not sure you can programmatically change aspects of nvim on the fly, and even if so, probably not a central component of nvim experience. M-x in Emacs is much more powerful than : in (n)vim.
Yeah, once you use threading macros, you are like "I want to convert everything in clojure to threading macros". Then you look at Forth, and you are like "Oh".
I care about the process of determining truth. If one does expert deferral, then they should do so properly. Sadly Nature is expending their social capital as a scientific journal to pivot to a typical news organization.
If one is up to date with sc news, this article should not affect their beliefs.
But maybe some people are happy that they can share an article from Nature to convince their friends.
It's sad to see people accept the credibility of this article simply because it's from Nature. The author himself is a freelance science journalist (with no real expertise in the field), so this article is not worth any more of our attention than many twitter threads.
"Bug" and "fork" are industry standard terms, "stories" are not. Plenty of frontend developers exist who don't know the term.
Overloading is fine. Ambiguous use of an overloaded term is not. What is one to think of when they see words like "write", "stories", and God forbid, "book"?
I also hear Scapple is good. Everything else is overengineered ime.