reuben364

There is also the tool of taxation and fines, which while in turn are backed by a threat of violence are not the black and white which you allude to.

And then Google slowly built a monopoly on browser implementations. Interoperability isn't appealing to corporations when users don't have much of a choice on using your platform.

Curious what your thoughts are on the paradox of tolerence? Google and the person hosting a static blog on a server in their basement are not the same.

Your "adverserial" mathematician phrasing made me chuckle at the the thought of a future where you have cybersec jobs in automated journals to prevent shady academics from using kernel bugs to spam fake submissions.

Yes it captures the essence, but if you have a category of ZF sets you still need to demonstrate that a product exists. This is just a possible product (along with its projections).

One distinction in Nix vs Docker is that Nix has a dag structure as opposed to a singlely linked list structure of layers.

The "writeText" function produces a derivation (basically an atomic build recipe) that produces that file. The crux of nix is that you make deterministic derivations, and then you can always refer to the results of a derivation from the hash of the derivation and its inputs.

What nix adds is glue logic to chain these derivations together in a way that preserves reproducibility of the individual imperative, but deterministic, components.

Unless you are using something like recursive-nix, you can completely evaluate the nix expression without building any of the derivations.

I deeply regret the courses I barely passed. And the courses for which I had prior knowledge to pass comfortably but not engage on the nuances.

Surely the frequency of the vibration matters too? I would suspect that motorcycles will be closer to the resonant frequency of the springs. I don't pretend to understand enough to say with confidence though.

I had a friend that had a record linkage problem which interested me and so I dove down a rabbit-hole of Markov logic, but didn't see any mention of Naive Bayes approach when doing so. Although I don't really have any expertise in the area anyway, so it would be easier for me to miss.

An example from South Africa: https://en.wikipedia.org/wiki/Searching_for_Sugar_Man

Your description of neural rendering techniques reminds me of a video (https://www.youtube.com/watch?v=6aXx6RA1IK4) where someone used a genetic algorithm to represent videos in Geometry Dash levels.

My CS degree (University of Cape Town) was basically a software engineering degree with a light sprinkling of theory. Basically our only proof that I remember was the the halting problem, and it was really only the basic idea with not much rigor.

We covered data structures & algorithms, concurrency, schedulers and virtual memory but it wasn't very math heavy. We have one full semester on software dev cycle and one for UI and mobile app development. Our final project was a group project to assess applying software dev cycle in a team. As far as I'm aware the CS department has a sizable HCI group.

I remember in first year with Python they taught the students to parse integers with `eval`.

Well one thing programmers do often due to the complexity of formal proof is random property testing instead. Mathematicians do so too, which is why the Collatz conjecture is a conjecture in the first place. There is an alternative to Software Foundations that uses randomized property checking. It would be interesting to have a hybrid system where we independently give specifications and then decide whether we wanted to formally prove them or just do tests instead.

At the worst of times, when I had a university assignment I would sit at my desk to do the assignment and physically feel a repulsive force from my work. Like a really strong gust of wind.

And now I have unlocked middle school memories of staying up all night, alternating between lying down from exhaustion to forcing myself to sit and write a few words each round for my English essays that day.

With my ignorance of the python packaging ecosystem, I was always under the impression that requirements.txt was the version constraints, not the lock file.

Isn't dt, to delete up until and df, to include. I'm guess either you have config or it's so ingrained in muscle memory that there is a mismatch between what you type and what you think it is.

When I played piano there was a point where I could play a piece without thought but couldn't parse the sheet music or know what my fingers were doing anymore.

Whoops, forgot to eta expand.

Trying out the thing, and since this is ycombinator after all:

  type Lazy<A> = () => A;
  const lazy = <A,>(f: Lazy<A>) => {
    let thunk: Lazy<A> = () => { throw null; }
    thunk = () => {
      const y = f();
      thunk = () => y
      return y;
    };
    return thunk;
  };
  const tap = <A,B>(f: Lazy<(a: Lazy<A>) => Lazy<B>>, a: Lazy<A>): Lazy<B> => 
    lazy(() => f()(a)());
  
  const ap = (f: any, a: any): any => tap<any,any>(f, a);
  
  const y = <A,>(f : (a: Lazy<A>) => Lazy<A>): Lazy<A> => ap(((x: any) => ap(ap(f, x), x)),((x: any) => ap(ap(f,x),x)));
  
  type Cat = {
    name: string,
    friend: Cat,
    prefersDryFood: boolean,
    foodPerWeek: number
  };
  export const cat = y<Cat>(self => lazy(() => ({
    name: "lol",
    friend: self(),
    prefersDryFood: false,
    foodPerWeek: 4,
  })))();

Breaks typescript though. Also, the laziness won't work here.

1. Haven't read too deeply, but aren't we working with FOL in this type system anyway (Well, Henkin semantics of HOL, I believe)

2. I guess the major semantic difference is that in one, you define a family of PERs for terms in a given type, giving each type separate notion of equality. In the other you define equality over all terms and types are just a predicates on terms. I honestly am not well versed enough in logic to understand what it means in that sense.

If you want a more expressive logic, use a language with dependant types. Although I wish to see more powerful type systems become more mainstream, I don't expect every language to aim for that.

I wonder what the optimal encoding is given a list of banned words for any substring of a message.

ZFA (1908) had urelements. You can just partition your urelements if you want distinct "types". Union across those would be disjoint, but within would be standard set union. Even in type theory you have Church VS Curry style as to whether you consider terms as inheritly belonging to a type.

Asking here because I can't find the the right google keywords. I see that m.reddit.com no longer works. Has it been that way for a while?

EDIT: It's been redirecting to reddit.com since at least 2021

You still need a way of normalizing expressions that is consistent with your runtime. To say that types ((x: bool) => F<true && x>) and ((x: bool) => F<false || x>) are the same, wrt judgemental equality, requires normalizing both to ((x: bool) => F<x>).

I saw rumblings about the AMA maybe beating the most downvoted "Pride and accomplishment" comment. Thinking of that I just yesterday got Diablo 4 and realized just how normalized always online, microtransactiony BS has become. Maybe Reddit too will not so slowly boil the frog.

Yes, but the point is that you are giving a constructive existence proof for that bound. You asked for why there are so few total languages. The answer, as far as I'm aware, is either brute force on a fixed amount of memory or giving provable bounds either by decision procedure on a restricted language or having to manually give a proof on a more expressive language. Is that that an answer to your (presumably rhetorical) question?

I guess the alternative is just bounding the number of instructions and proving inside or outside your language that it is sufficient for your program.

BRB, implementing a x86 interpreter with O(2^n) memory overhead.

While Lean4 is meant to be much more of a general purpose language than it's predecessor, it is still built with being a proof assistant in mind. That being said it is self hosted and has been in development and use for quite some time, which says something of it's readiness.

Tooling around it great (it is installed with a rustup fork called elan).

As far as performance, it uses a particular version of ref-counting that allows mutation of unique references based on run-time tracking rather than compile time. If you accidentally keep a reference to an array and modify it, then you end up copying it rather than just mutating it.

Perhaps a more generous interpretation is that just because a self-driving performs better than humans overall doesn't mean it performs better the specific situations you drive in. Though even then I think it might be dubious.

Ah, you don't need linear types for that. Linear types will prevent you from duplicating or discarding values, but all you need is to only allow "final state" values to be used in your API.

Also a reminder that I should read articles before commenting.