Mathnerd314

"Bailout: How Washington Abandoned Main Street While Rescuing Wall Street", Neil Barofsky, page 157

Note though that he is only quoting "off the record" conversations with Treasury Secretary Tim Geithner

Seems like basic "you expected that, didn't you?" sort of findings, although they did verify the absence of a lot of correlations. But it's kind of cool that they can directly measure how much impairment a bad night's sleep causes.

> One course of action that we chose not to pursue for ethical reasons was publishing actual packages using hallucinated package names to PyPI

I mean, this makes sense from a security perspective. But from a language usage perspective, if there is a missing package that would be super-useful, then implementing and publishing that package would be a win.

I'm curious what the package names were, they seem to have deliberately omitted any package names. Maybe there are some good package ideas in the 19% of names that were hallucinated by multiple models.

It seems OK, for a small model. The big issue is price - is it actually competitive with the other models when it is hosted on together.ai or other API services? Which we will presumably find out at the Oct 24th event.

Don't forget externalities. E.g. you can get a fee-free bank account with fee-free cash withdrawals, courtesy of the bank being able to loan out that money under fractional-reserve restrictions. In that sense transactions can pay for themselves. Presumably nobody would print money if it wasn't being put to use. Hence, novel currencies can enable novel business models and potentially do more than just lower transaction costs in a zero-sum way. (Admittedly the value of such business models at present, e.g. crypto scams, is somewhat debatable)

I think there are use cases for open source. E.g., you write some throwaway code, and want feedback - the obvious strategy is to publish it open source. It becomes clear that the app you are working on is not a viable business - maybe the code is useful to someone else, and if you were tracking licenses properly it costs nothing to publish it. Some types of software, like compilers, I simply wouldn't trust if they are not open-source.

But it's also true that it is easy to buy into some strange ideas like "sharing is caring" and end up going past reciprocal altruism and into territory where you are working for free.

> unbiased factual reporting

I don't think that has ever existed, but the closest I've found is Wikipedia. It is surprisingly detailed, particularly on current events.

I think it's a bad title. The moral is more like "work on everything you can think of but don't release anything until it's ready. And some projects will never be ready, but that's OK - you can look at them 30 years later and release them on github for nostalgia." ChatGPT summarizes it as "Build Fast, Ship Never (Until You Do)"

I meant the actual court document. There is an electronic system, https://www.courts.go.jp/saiban/online/mints/index.html, but I am not sure it is public.

Does anyone have the actual filing?

Probably as a business expense it can be deducted from income for the business + no increase in personal income for him. It's not free but is something like a 50% savings vs. paying himself and buying it personally.

There is uiCA, it achieves an error of about 1% relative to actual measurements of basic block throughput across a wide range of microarchitectures. And then FACILE, similar to uiCA. I don't know of any compilers using these more accurate models, but it is certainly possible.

There is some noise in the rankings, I think the answer is it doesn't. It is highly overfit and my guess is you won't get the STS visibility effect with e.g. minor changes in the descriptions of unrelated products.

2020, judging from the URL.

> the purpose of TLA+ is to help design and reason about executable things

> execution - [this is not one of] the things that TLA+ helps with.

I think there is a depth limit on HN so I'm just going to stop after this. No, I do not have a "real question". I made a statement, that TLA-PL is a programming language. You still not have agreed or disagreed with this statement, just said that you find it "a distraction" and "confusing" and "not really what you have in mind". Well, un-confuse yourself and present an opinion on its veracity. I don't think it's a distraction because it is a point Lamport brought up in TFA.

This thread has been going on, let me try to distill the points:

- TLA+ is "definitely not" a programming language (per you and Leslie Lamport).

- TLC has got nothing to do with TLA+ (as a mathematical formalism). TLC is not "an implementation of TLA+". (per you)

- TLC is a tool that can process "something like" TLA+. You say "subset", but it seems to me it is not a strict subset, because special operators like "Print" have different semantics. Let's suggestively call what it processes "TLA-PL". You mention additional configuration but the configuration can be empty so it's really like a pragma or compiler option.

- TLC can evaluate and print TLA-PL expressions in a REPL. (per the repo I linked)

- TLC and TLA-PL could be extended to implement typical programming language primitives such as input, a Java FFI, etc., fairly easily (per observation of the source code)

- TLA-PL is not TLA+, because it is not a rich mathematical formalism, like a drawing tool or English. The purpose of a TLA-PL document ("program") is to produce an output that's either TRUE or a counterexample, although there are other modes of running TLA-PL. In contrast, the purpose of TLA+ is itself, and a TLA+ document ("specification") has no output - the deliverable is the document.

Now it is true that other programs have REPL-like functionality, like the calculator you mention. Generally the benchmark between calculation and programming is Turing completeness, e.g. whether the language can express recursion. In a calculator, if you add a few statements like stack push/pop and command names, suddenly it is a "programmable" calculator like the HP-32S, and Turing complete, and the calculation language becomes a programming language. What about TLA-PL? Naturally TLA-PL expresses recursive statements easily - it is almost trivially Turing complete and hence a programming language. And it is clear by definition that TLC is an interpreter for TLA-PL, so TLA-PL is even an implemented programming language. This is what distinguishes it from the majority of formalisms, in that most formalisms (English, mathematics), although potentially usable for programming, do not have working implementations. It is not a requirement to be a programming language that everything written in the language is computable - Verilog, for example, is actually quite flexible as a hardware synthesis language, allowing one to write unsynthesizable programs, but in practice people simply avoid writing these programs when doing hardware synthesis. Similarly I am sure that valid-looking TLA-PL programs will look correct but nonetheless fail to run under TLC due to limitations of the model checking and so on.

Now it is true that TLC, although it implements TLA-PL, is not an implementation of TLA+, as by definition TLA+ is like mathematics, infinite in scope, hence not implementable. I would argue this also means TLA+ also isn't even definable, but that's a separate issue. Similarly, Leslie Lamport's purpose in creating TLA+ was not (and is not) to create the programming language TLA-PL, even though it exists. This to me is what you're getting stuck on. As a programming language designer, what I care about is TLA-PL. To me it is clear as day that TLA-PL exists as a programming language and and could be turned into a useful one given sufficient effort to modify TLC. In contrast, all I hear from you is "TLA+ this", "TLA+ that", "pay no attention to the working implementation of TLA-PL". But as I said, I don't care about TLA+ - as soon as you say it realizes unrealizable things, you are speaking poetry rather than programming language design. There are tricks like lazy evaluation and so on where a computer represents "unrepresentable" objects symbolically and thus can manipulate them, and from my understanding some of these tricks are implemented in TLC and TLAPS, but it seems clear you are talking about a level beyond this, where a TLA+ specification cannot be evaluated even with symbolic tricks.

Say that when I need to run some program and I have an ARM processor but the only binaries available are x86...

> If you read the TLC documentation, it makes it very clear that it is not TLA+.

Fine, clearly you are missing the point I am making about how languages become confused with implementations. Just s/TLA+/TLC/ in all the above. Is TLC a programming language implementation or not? Consider for example https://github.com/will62794/tlaplus_repl which evaluates TLC expressions. At what point is there sufficient programming language functionality for you to become convinced that TLC is a programming language?

> the PrintT operator is defined in TLA+ like so

No, it is defined like so: https://github.com/tlaplus/tlaplus/blob/0dbe98d51d6f05c35630... This is the same strategy that Haskell uses for its primops, a placeholder file and implementation in another language. I guess you didn't understand my point that it would be easy to extend TLA+/TLC to more primops, like memory, a Java FFI, and so on, making it a fully featured programming language. I don't care what "the TLA+ language" is, C++ implementers regularly toss the spec in the dumpster and just like you have C++/LLVM and C++/GCC there similarly is a dialect of TLA+ for each implementation.

You can write hello world in TLA+:

Main == PrintT("hello world")

You can't write much else, because print is the only implemented command (no input commands even), but it's clearly not just a program that reads newspapers out loud. There is an execution semantics and so on, as found in typical programming languages. It would not be hard to add input, implemented as a "hack" along the lines of print, although of course TLA+ is nondeterministic like most logic programming languages so there is some tricky semantics.

I'm not saying TLA+ is a good programming language - it is more along the lines of Brainfuck or TeX, "use it only out of necessity or masochism". But at least in my book it is undeniably in the category of programming languages.

> It's not a program

It is a program when I can do java tlatk.TLC someprogram.tla.

You say `3 * 3 = 9` is a TLA+ specification. Well, here is a Prolog program: 3*3 #= 9. Is there a difference? No. The output when I run the Prolog program? "yes". The output when I run the TLC program? I haven't tried, but it is probably similar to "yes" or "no". It is in this sense that you can run TLA+ programs and get a relatively small output of whether it checks. Maybe you don't consider this programming, but people have done more with less, e.g. lambda tarpits where all that happens is lambdas reduce to more lambdas. In contrast the value space of TLA+ is quite rich, it is only the usability of it that is limited because Leslie Lamport continues to insist that TLA+ is "not a programming language".

Actually the converse is true: Lean and other projects have formalized most mathematical theorems. But it is an "additive" process - it is easy to paraphrase a formal Lean theorem as colloquial mathematics, but it is hard to formalize colloquial mathematics in Lean. Some of this is due to Lean not being as developed as it could be, but also there is simply that some "theorems" in mathematics are simply "wrong" in that they make unstated assumptions and handwave away important parts of the proof. It is in this sense that programming is less expressive than mathematics, in that you can get away with writing things in mathematics that you can't get through a theorem checker. And this is conversely why I say that programs for theorem checkers are executable - the requirement to pass a theorem checker imposes constraints on proof structure and such that is not found in the "natural" language of mathematics. The lack of these limitations is what I would say the limitation of mathematics is, that even well-known proofs are not necessarily completely "true" due to unstated assumptions.

Now regarding TLA+ vs TLC, I am not clear what the utility of a TLA+ program that cannot be checked with TLC / TLAPS / etc. When you say "prove" a TLA+ program I first thought this was formally checking it with TLC / TLAPS / etc. But it seems you have a different notion of proof, some sort of handwaving "it looks right" notion. From my perspective this reduces a TLA+ program to a piece of writing, since nothing automated can be done with it. You might as well say "You can express every theorem in ZFC in Java by writing it in a comment" - it is not an informative observation. The interesting TLA+ programs are the ones that can be checked with TLC / TLAPS / etc., and to the extent one can work with these programs programmatically, TLA+ is a programming language.

ChatGPT does just fine with math. I wasn't joking...

I looked for this "direct address". All I can tell is that he's repeatedly contradicted himself. http://lambda-the-ultimate.org/node/4922#comment-79370

TLA+ is executable in the sense of Prolog: there is an algorithm (the TLA+ implementation) that takes a TLA+ program and produces output. Most mathematics is not executable in this sense, you will have a very difficult time doing anything useful with the PDF's of published math papers. Math is a natural language, TLA+ is not.

And I would agree, TLA+ as a specification is different from TLA+ as an implementation. I generally disregard specs, I was talking about TLA+ the implementation when I said it had no future. It seems it will be in perpetual maintenance mode with barely any new features.

Regarding simple vs. easy, I challenge you to argue that temporal logic is "simple" in any sense of the word.

> in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all.

Well, in TLA+ you can write programs that run forever (or at longer than you'll live) and don't do anything like "model check" or whatever you want to call executing TLA+, even though they are perfectly sound mathematically. This should make it clear that TLA+ is not maths.

> Simplicity is a major goal of TLA+.

Is TLA+ simple? I find this hard to accept.

> TLA+ isn’t a programming language; it’s mathematics.

Mathematics is not executable, though, whereas TLA+ is.

> TLA+ [is better] for its purpose than a programming language.

"TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior."

"specification of system behavior" sounds like a programming language to me. A systems programming language, even.

All this is to say that it seems TLA+ really has no future. If there was a future, like a goal or a roadmap or something, it would be outlined in this document a lot more clearly - whereas, instead, it is more like "nope, everything's good, no changes needed", even as the language appears nowhere on the TIOBE rankings.

I get that the demos are interactive but for me at least a 2 minute video would be more useful in explaining what the product actually does, unless you really think you can demo the software using itself. There is not much point in ungating when I don't even know what the product is. Signing up is not a big deal, it probably is just that users still had no idea what the product was and weren't comfortable creating an account. And it seems it still requires an investment because the chrome extension is the main use case and has to be installed.

Bookmarked it though, I might end up using it.

It is a 2024 model, for comparison https://github.com/danielgatis/rembg/ uses U2-Net which is open source from 2022. There is also https://github.com/ZhengPeng7/BiRefNet (another 2024 model, also open source), it's not too late to switch.

I've been working on an exercise database, using ChatGPT. I got a list of all the interesting exercise qualities, then I turned those into measurable data fields, and now I'm organizing the 600+ fields. The goal is to build the ultimate exercise database with 50K+ exercises.

But lately I took a break and worked on running (GPX run file analysis) and habit tracking. The eventual goal is to package it all together into one integrated PWA / mobile app.