The runtime performance is most probably worse than yours. The goal of this project is a minimal specification that a reviewer can trust. See section in readme on performance and how it could be improved while still keeping formal guarantees, but would mean a reviewer having to trust axioms on floating point numbers:
https://github.com/schildep/verified-3d-mesh-intersection#pe...
On a readme style note, please spend more time explaining the algorithm and less time bragging on how amazing vibe coding is or how Lean has a zero trust proof.
I presume the new advance is claim that verified-3d-mesh-intersection is verified and not the claim that vibe coding can replace hand proofs or that the claim that lean4 can be correct without trusting llms.
> The "It's not X -- it's Y" pattern, often with an em dash. The single most commonly identified AI writing tell. Man I f*cking hate it. AI uses this to create false profundity by framing everything as a surprising reframe. One in a piece can be effective; ten in a blog post is a genuine insult to the reader. Before LLMs, people simply did not write like this at scale. Includes the causal variant "not because X, but because Y" where every explanation is framed as a surprise reveal, the em-dash dismissal "X -- not Y", and the cross-sentence reframe where the same noun is negated then repositioned: "The question isn't X. The question is Y."
The information is hard to read because I had to run an https://tropes.fyi/ filter over the essay to make it readable.
I don't mind the AI tropes that much, the issue is more that the amount of information is exactly what was in the prompt but the AI manages to add many words saying nothing.
> The screen we shipped in January 2016 made two statements at once: pick intent said your plan matters, while the queue attached to it said what a ladder measures is negotiable. Players parsed the two separately, with total precision. They kept the first and burned the second down.
This is a classic AI construction to me that reeks of Markov chain thinking. The first half is probably the prompt to some extent. The second half ... doesn't actually say anything if you read it closely. Humans can write this sort of content-free fluff but usually they do it for a strategic reasons and not when they're trying to explain something. "Players parsed the two separately, with total precision" resolves a question of clarity that was never raised and for which there is no evidence of problem or solution (it is probably trying to say they understood and disregarded ... something that was basically elided). Then we have a tortured metaphor that doesn't tell us anything about what the players did.
It is quite tiring to read because you have to re-read things a few times to confirm that it didn't say anything and it isn't pretty wordwork worth reading on its own. Reading this is an exercise in trying to reverse-engineer the prompt.
Question to you all, muds tends to have a unix style interface, has anyone done a replacement for this uiux that fits … the class of 2019 first year computer science student that doesn’t understand files and needs a different uiux.
I'm not sure I understand correctly, muds are text based but not file based. But there are several mud clients available with different features. Most include an auto mapper for example, you can connect through different specialized protocols to your favorite mud server.
I mean, that’s a MUD for you. It’s inherently text based. It’s of the golden age of the internet where passing the UX bar meant you earned your place in the community.
The genre opened doors for MMORPGs like EverQuest. If you want something modern and polished there are no shortages of other games.
I think part of the nostalgia for MUDs is a nostalgia for the era of the internet where communities were small and special. Everyone has a discord now. It’s all so samey. Bring back the quirky hobby communities run by the users.
I am not sure I understand your question- MUDs have a text interface, somewhat similar to a command line. It wouldn't be a proper MUD if it had a graphical interface- there are plenty of games out there that do this like Baldurs Gate. The files part of your comment I don't understand either.
If a computer science student doesn’t understand files, that should be one of the things they are taught. What’s the point of being a student if it isn’t to learn?
My college roommate was really big into MUDs, one particular one anyway. He wasn’t a super techy person, it was pretty much the only thing he did on his computer.
Ignoring all the other distinctions between lisps, the main difference between lisp-1 and lisp-2 (or lisp-n) is going to be how clean your code looks when you lean into the FP style. In a lisp-2 you'll need to do something like this:
(defun apply-twice (f x)
(funcall f (funcall f x)))
(apply-twice #'1+ 2)
Versus this with a lisp-1:
(define (apply-twice f x)
(f (f x))
(apply-twice 1+ 2) ;; assuming 1+ is defined
But there are so many other differences between the lisps in the two categories that this probably won't be the deciding factor for most people.
I am a strong proponent of Lisp 1, primarily because the distinction between functions and other types of values is artificial. Functions have first class semantics in Lisp 1 and Lisp 2, but Lisp 2 makes you denote them differently but in an inconsistent manner.
Lisp 2 advocates typically make a few arguments. One is that having a separate namespace for functions makes it clearer when you are using a function vs another value. The second is that the evaluator has less work to do when examining the head of a list - it needs only look in the function environment, not the full environment.
On the first subject I must disagree - you can bind a function to a regular variable and then use that variable everywhere (except in the car of a list representing a function call), so for most positions in a set of expressions you don't really get information about whether the object being denoted is a function or not.
I suppose the second point is somewhat valid, though I suspect if you benchmarked interpreters and compilers it would barely matter. As a person who favors functional programming with a lot of combinators, I find Lisp 2 introduces a lot of pointless noise in the syntax for no reason. And I fundamentally just don't see functions as significantly different sorts of values, so I find the syntactic distinction bizarre.
The argument is: if you don’t have hygienic macros, a Lisp-2 is going to be less brittle than a Lisp-1.
The classic example is, imagine you have a function with a local variable called “list”, common enough. Now imagine you invoke a macro inside that function which generates a call to the built-in “list” function - also common enough. In a Lisp-1 without hygiene that breaks - your local definition shadowed the built-in; in a Lisp-2 or hygienic Lisp-1 you’re in the clear.
People should never use non-hygienic macro systems anyway, but even if they are using a non-hygienic macro, they should always use proper hygiene. Its kind of dumb to make the whole system weirder just to avoid issues which should never happen in the first place, in my opinion.
@nathan_compton, your sibling comment to what I'm writing now is [dead] (not [flagged]) but you're not shadowbanned, newer and older comments are still alive. I vouched for it but it's still [dead], you may want to reach out to the mods.
The usual argument I've seen in favour of Lisp-2 (I personally don't care as much about the function namespace as I do about the type namespace, which I find much more important) is that you can name an argument a conflicting name with a function without the conflict interfering with the code you would write:
(defun merge-sort (list before?)
(declare (type List list)
(type Function before?))
(flet ((merge-2 (a b)
(declare (type List a b)
(merge 'List a b before?)))
(unless (null list)
(reduce #'merge-2 list :key #'list))))
(merge-sort '(1 9 8 2 3 4 7 6 5)
#'<)
Instead of having to name lists 'lst' or something. Which is pretty much personal preference anyway.
In a language which doesn't normalise the case of symbols you could in theory work around that by capitalising or upper-casing either the function or the variable, but that's still not a particularly elegant solution.
Having a separate namespace for functions is silly in that it only saves you from a small set of variable shadowing problems. It’s a hack, not a serious solution.
personal taste, for the most part. I like the thought of a single namespace, it fits my intuition from pretty much every other language out there, and I like how the code looks when I can pass functions around as though their names are regular variable bindings to an underlying function object.
I hate having to come up with different variable names than `list` so I don't shadow the function `list`. Repeat that for a lot of common words: count, first, length, map, max, min, search, string; that you would then actually consider calling said function after declaring a value. Happens to "list" the most, but definitely the others on rarer occasions.
IMO if we look at Lisps today the question looks more like: SBCL, Chez Scheme, Racket or Clojure.
Common Lisp and Racket are Lisp-2s but honestly, the namespace thing seems like a minor difference compared to all the other features that differentiate them.
Lisp-1 has the wart that it models special operators as bindings in a variable name space. So a form like (print let) actually resolves let to a binding to a special operator, and then has to be somehow pronounced as nonsense. And you can block let from working by binding that as a variable name. Allowing variables to shadow the basic operators of the language is quirky.
Would you want to use a weird POSIX shell in which "for x in *.jpg; ..." stopped working because you assigned "for=42"?
Yet Lisp-1 has a notational advantage for programs that work with functional values; programs that indirect upon functions are more succinct, free of "shim" operators for lifting values out of the function binding space, or requesting application of a function value.
In the TXR Lisp dialect, I worked out a way to have the notational convenience, without bringing in the Lisp-1 issue.
1. The substrate, including macro-expansion logic, is thoroughly Lisp-2.
2. When a compound form is written in square brackets, it indicates that immediate elements (those constituents that are symbols) are to be looked up in a single namespace that is a merger of the function and variable namespaces according to precisely documented rules. This is not recursively applied to the form; its arguments that are compound forms are not treated this way unless they use square brackets.
3. Macros are not affected. In a form [a b c ...], the element a is neither recognized as a special operator or as an operator macro. If it is a symbol, it is either a variable, or a symbol macro.
4. [ ... ] is a surface syntax with a straightforward representation: the (dwim ...) operator. The above semantics is thoroughly baked into the macro expander and correctly treated at all necessary levels of the language: the handling of lexical scopes at expansion time and compilation/evaluation.
This system leaves mainly just one small infelicity. The merged 1+2 namespace is not available in certain contexts when it would be handy. Like say we are writing a function that takes a functional argument, that we would like to default:
because the (test-fn equal) syntax is not a form to be evaluated; it is just notation within the parameter list which has not been equipped with support for the alternative brackets/dwim structure. The way to do this is:
fun* is like Common Lisp's function* operator. It's one of the few instances you ever have to use it, the others also being situations like values in binding constructs such as let. It is not worth complicating things to provide a way to take the fun out these situations.
Its not a computer, its a small device. You dont have many unknown peripheral you dont have other programs. The memory and peripherals are there, just use them. Heap is complicated ? Preallocate everything. A peripheral is not used ? Just leave it there. Security ? Of what ? Thats the appeal of those devices.
Your comment got downvoted but I think there's deep truth in it. I've been decompiling GBA games from my childhood and it's remarkable how engineless they seem to be.
A llm emulating a person is why many of my used sites banned llms due to scraping bandwith costs
Is this about access or accessibility to claude (for example)
I am sure the entirely of human computing knowledge is not that big.
reply