anyfoo

Yeah, but that still doesn’t mean there aren’t theoretical bugs. Testing every input would effectively mean testing every stimulus, which is combinatorially impossible. You might still have subtle timing bugs, bugs with very uncommon instruction sequences etc.

But my point was exactly that the (extremely vastly) smaller subset of tests that you performed is more than enough to proclaim a CPU to be “working”.

Do you test every possible input/output combination on any CPU?

No, because that would be impossible.

You perform a series of more specific tests. In this case, it's "working" in so far as that Super Mario Bros. appears to be playable, for example.

Does not mean that it behaves perfectly according to some spec, or identical to another CPU (like the NES's 6502), of course, but it's clearly a working CPU to some 6502-compatible extent.

This moving of goal posts whenever correctness through type systems is being discussed is a bit tiresome, because it quickly leads to such ad absurdum corner cases.

Yes, you are all correct. The compiler may have a bug. And if it does not, then the type system may have a problem. And if it is formally verified, then the theorem prover might have issues. And if it does not, then the very math it relies on may be wrong.

But what do we contrast this to, what is the alternative to correctness through the type system? Almost every time, when it isn't "nothing", it's "tests". We rely on tests to test whether the program behaves correctly.

And as we all know, quite in contrast to type systems and their checkers, tests are always error-free, complete, and sensible?

Did you give him the ability?

That's for the FM baseband signal, not the audio. Among other things you're doing here, you're basically treating a stereo signal (plus a pilot that effectively contains no information, plus an extremely low bitrate RDS stream in an extremely inefficient way) as one monaural signal.

But maybe there's a use case for replacing an AES192 signal carrying the full FM baseband signal over ETH-67? I'm not sure it's the correct fit, though.

No, I'm not misunderstanding, and you are pushing goalposts. The majority of programs above a certain size would benefit tremendously if they were "matching a specification". Sure, the specification itself may not be fully correct, but a lot, if not most bugs, are code that would go against such a specification.

> Also, just think about this: what bugs have you had in your software historically? How many of those do you believe would've been prevented by a type system like Haskell's??

I program Haskell all the time, and I encounter "non-bugs" where the compiler prevented me from doing something, which other languages would not have, on the regular.

> (though I do use typed languages like Java and Kotlin)

Those are not even close to a Hindley-Milner based type system like the one in Haskell.

How so?

I don’t use this one, because I remember when long, long ago it was in some random IP address block belonging to someone, and this particular address didn’t reply to ping.

Likely for good reason, even back then there would have bound to be lots of misconfigured endpoints trying to access 1.1.1.1, so just blocking it at the earliest point possible kept at lot of the annoyance away. Nowadays, it’s an anycast address, so it’s slightly less bad.

But for me, old habits die hard.

Can you produce those studies? Genuinely interested. Intuitively, I would have thought properly used Haskell prevents a lot of bugs by virtue if its type system, which allows for encoding internal constraints to a certain degree.

The extreme end of this is dependent types, which is so strong that it can be used as a foundation for mathematics itself, and is the principle that the Lean, the proof assistance, is used on. A Lean "program" is effectively proven to be bug-free.

That is insightful, thanks. I didn’t start caring about models until very late, so I genuinely thought GPT-2 was only a single tiny model originally.

And I now tried using it more as a “text completer”, and results are much better.

Be sure to send them an email first, so that you can arrive at the proper time for them to give you a tour. It is very, very worth it. One of the best museum experiences so far.

I've been playing with it for a bit, and I'm a tiny little bit surprised that they decided to continue pursuing that direction of research at all. What I'm getting from it looks like it could just be arbitrary sentence and paragraph fragments from the Internet, pasted together Markov-chain like.

I'm not sure I would have ever believed that something useful would come out of it, yet here we are.

It is, in every sense, incorrect. Which statement in this short snippet is "semantically correct"? (Better LLMs get this right, of course.)

I mean, they were both.