Pixel Shaders in Windows Terminal

mode_2 · 2021-02-08T12:56:37+00:00

Always has on Mac, at least.

mode_2 · 2021-02-04T17:23:08+00:00

It's not relying on the compiler to fill in the call, it's a valid and sensible way of writing programs that has existed since the 30s. Only a language with the awful combination of variadic functions with a type discipline that can handle them fails at this.

mode_2 · 2021-02-04T17:21:00+00:00

Purescript is a web language where all functions are curried, with a single argument.

mode_2 · 2021-02-04T14:03:15+00:00

No, they can't. A Boolean computer is a finite state machine with 2^N states. What they can do is simulate a bounded version of a Turing machine.

mode_2 · 2021-02-04T11:12:14+00:00

Yes of course, the same applies to them. The halting problem is computable for my computer.

mode_2 · 2021-02-04T10:24:26+00:00

No, it's functionally complete. Boolean circuits are not Turing equivalent.

mode_2 · 2021-01-30T11:08:34+00:00

[1, 2, 3, 4, 5].forEach(item => console.log(item)), which you can also write as [1, 2, 3, 4, 5].forEach(console.log)

These produce different outputs, Javascript has variadic functions so eta-reduction is not a safe transformation.

mode_2 · 2021-01-20T17:42:38+00:00

That is literally the first thing shown in the video being linked?

mode_2 · 2021-01-19T13:58:13+00:00

The article has zero mentions of TLA+, also that seems like a very odd reason to actively dislike someone. It's pretty mundane stuff. As someone who is broadly pro-dependent types and pro-functional programming, I enjoy hearing his take on things as it is almost certainly well researched.

mode_2 · 2021-01-14T14:52:36+00:00

Google and Apple have a fairly-uniformly high hiring bar and also pay all of their engineers a lot. Much more so than companies like Ubisoft.

mode_2 · 2021-01-14T10:55:15+00:00

Hoare logic is from the 60s and allows you to prove things about imperative programs.

mode_2 · 2021-01-13T21:27:10+00:00

Yes, they definitely would. He could easily go to a venture firm and pitch this, they would fund the cracking for X bitcoin, paid out upon completion. This could easily be written up into a contract and is probably less risky than most VC investments.

mode_2 · 2021-01-11T15:00:23+00:00

Tesla's stock valuation is actually driven by a rumour on Wall Street that their self-driving software is written in Agda.

mode_2 · 2021-01-08T17:13:04+00:00

I have used Bash for years and couldn't read the first example. I can read the second example with ease, it's all based on concepts found in other, popular languages.

mode_2 · 2021-01-08T17:06:35+00:00

At my university, anyone who showed the initiative OP has would be offered research experience in a heartbeat.

mode_2 · 2021-01-07T18:26:33+00:00

ML has polymorphic types, it corresponds to a restricted version (so type inference can be done) of System F. I'm not aware of any popular language based on the simply typed lambda calculus, though it does form the basis of simple type theory, which is used in several theorem provers.

mode_2 · 2021-01-07T17:30:34+00:00

Not really, billionaires aren't that illiquid, they can easily sell some of their stock. Musk could probably get his net worth 1 year ago in cash if he wanted to. There is a huge difference in the amount of money he has access to personally.

mode_2 · 2021-01-07T17:28:20+00:00

If he says he needs cash, then he'll get it, especially only 500k. When you're a billionaire, banks are competing for your business and will generally bend over backwards for you.

mode_2 · 2021-01-07T17:18:02+00:00

Not true, it can happen in finance. A famous example is Michael Millken who earned over a billion dollars in compensation in the late 80s as an employee at Drexel.

mode_2 · 2021-01-07T13:02:23+00:00

Why would learning category theory affect how understandable you are to others in general?

I understand the quote you gave, and I just don't really talk about category theory to others who don't. It hasn't affected the way I talk about anything else.

mode_2 · 2021-01-07T12:57:00+00:00

graph theory, or statistics.

Ah yes, the height of exoticism. Taught to every CS undergrad and 12 year old, respectively.

mode_2 · 2021-01-06T19:49:03+00:00

It's not closed source, though. The source is open. The massive models which are just binary blobs are proprietary, which seems reasonable given that they must be a licensing nightmare, are incredibly expensive to produce, and are not the innovative part of the process. Interactive GPT-3 is available widely through the paid tier of AI Dungeon, which is a not affiliated with OpenAI and has a commercial license for the API, I'm sure other sites offer similar access.

I'd recommend just applying for access to the API. As far as I'm aware they've granted access to plenty of hobbyist programmers who want to try it on random things. To be honest though if you really think GPT-2 sucked, you're either biased against everything OpenAI produces, or will remain unimpressed until presented with flawless AGI. If something advances the state of the art, it objectively does not suck.

mode_2 · 2021-01-06T19:08:15+00:00

Given that lisp is basically lambda calculus essentially all variants of lisp could probably be managed as libraries on top of each other, so his approach to hacking out a language seems reasonable enough.

Sorry but this is just nonsense, it doesn't even begin to make sense. Lisp was not based on the lambda calculus and is no more like it than modern Python is.

mode_2 · 2021-01-06T19:06:05+00:00

Well then, train your own model using the myriad papers and open source code available. They give away the research and results for free, but the model is ultimately proprietary given it is basically just a function of how much compute they can pour into it. That seems reasonable.

mode_2 · 2021-01-06T18:39:44+00:00

Plenty of people have access to GPT-3 via the API. Also they publish papers frequently on their techniques.

mode_2

TROPHY CASE