markusde

Nobody knows enough about the universe to say this.

Can confirm. Just graduated, and a significant chunk of my cohort is going or is planning to go south.

Mind, I don't get the impression that they want to stay in the states. I include myself in that camp, the plan eventually being to work remote for an American company from Canada.

An extremely brief google search tells me that controlled burns require firebreaks, knowledge of the wind patterns (something called a downwind backfire?) and presumably continued monitoring/support from firefighters to actually be a controlled burn over the area that needs it.

I think what you're describing is a total fantasy.

(jokingly) yes, in Haskell: https://clash-lang.org

I don't think that this is right. A programming language is useful to programmers if it's oriented around the structure of the _problem_ and not just the structure of the _physical machine_. For some tasks these coincide (especially if you care about performance) but I frequently find myself in situations where functional code is simple and the machine is irrelevant.

Yeah, I'm cautiously excited about how AI and FM might work together. I don't think LLM's can ever be trusted to verify programs itself, but anything which can reduce the annotation overhead for programmers is a super useful thing!

Interesting-- thanks!

Aha-- so then HVM allows a more efficient reduction of some lambda terms, but is not intended to replace something like GHC core?

What is the subset of lambda terms which HVM can (soundly) evaluate?

> A caveat of this technique for reducing lambdas is that it doesn't exactly match the behavior of the normal lambda calculus. While it might reduce the same as the normal lambda calculus in many cases, it doesn't always. And that's totally fine, it doesn't need to match perfectly to be useful in it's own right.

This seems like a serious problem for something trying to be so foundational... I'm kind of surprused the author doesn't go into more detail about it. Why is this fine? If not for evaluating arbitrary programs, what is HVM useful for?

IMO after the first section the headings in the post are misleading: - A functor is "not a functor" because not all endofunctors on Hask can be written as Haskell Functors. - A monad is "not a monad" because you can implement a monad without satisfying all the monad laws.

I don't think either of these statements _really_ evidence the claims the headings make. Good post though, I always find that it's useful to think about the subtleties between mathematical objects and their implementation.

I think I see what you're getting at. A few final points:

- There's a subtle difference between "infinite" and "unbounded". Turing machines use at most a finite amount of memory after any finite amount of steps (the tape always ends in an infinite sequence of empty cells), so a machine which starts with one cell and allocates one new cell every step is equivalent to a TM.

- Unbounded memory is always assumed for analyzing complexity. If not, all algorithms on all computers are O(1)... which is more or less the line of inquiry you seem to be going down. All algorithms being O(1) is not a useful measure of complexity.

- We can model finite but unbounded memory IRL: if a program is allowed to allocate new machines on a network (and also pause until that new machine is online) the amount of memory can grow dynamically to the scale of the universe.

- Undecidability is defined on Turing machines, so we definitely can say that some theories are undecidable. No stronger method of computation which can also be physically implemented is known to exist.

edit: typo

> I'd argue the complete opposite. It's very meaningful for me to distinguish whether a program works correctly, crashes due to running out of memory or loops forever.

Fair for many applications. I work with computers that write proofs.

> Yet being the key word here. As far as I know it's not proven that it's impossible to build a time-efficient algorithm, only that (as far as I understand) it's unlikely unless P=NP. But there's another issue here as well: we don't know whether P=NP.

There are worse complexity classes than NP, for example EXPTIME, which we know are not P by the time hierarchy theorem.

> How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case?

Well, not me! Formal methods and program synthesis are alive and well, but it's important to researchers in these areas to understand what parts of our work are decidable and what aren't. I should mention that Writing efficient SMT solvers is an important aspect of this even when the theories are undecidable, and tailoring tools to real user patterns can really blunt the problem of undecidability in practical use cases.

While technically correct in several ways, this is a pretty naive take on the topic. A simple counterexample is trying to decide whether a program which computes the Collatz conjecture will always halt (which is equivalent to proving the conjecture itself). Proving it always halts (or crashes) in some fixed amount of memory is insufficient for saying anything meaningful about the program: we oftentimes care about the mathematical object a computer is modelling, not just the computer itself.

Furthermore, it is true that computers have a finite number of states, but this number is intractable for most problems in verification. There are several well known cryptographic problems that take on the order of the lifetime of the universe to solve in bounded memory... if you're trying to write a program to verify one of these algorithms the boundedness of memory will probably not help you much.

Is lifetime syntax so terrible? Personally I like that all the subtyping relations are in the same place (lifetime outlives, polymorphism etc) and that they can be written inline until complicated enough to justify a ``where`` block.

Yes-- working right now on a tool that uses Rust compiler internals. A previous contributor made a module with a clean interface to almost all of the compiler analyses I needed and without much compiler cruft. Coming across it was a borderline religious experience.

This is totally right. There are two kinds of classes: those with a specific set of learning outcomes to meet (eg. a prerequisite course) and those where by the end the in-scope knowledge is essentially unlimited (eg. courses where it's not unreasonable to prove named theorems on homework or exams). The former should be graded with 100% being all the knowledge, the latter in a way that gives a fair distribution and then scales.

Of course, my fellow university students always push back on me when I support the latter :) At the risk of armchair psychoanalyzing, I think a lot of them don't want to reckon with the fact that there's such an overwhelming amount of information out there and so many perspectives to explore it from that "100%" in say introductory topology is almost completely meaningless as a measure of how much topology one actually knows.

I mean it does include "programming with abstract data types"

More classic FP papers could have been added but honestly this doesn't seem like a bad little collection!

It's been half-working, half-broken for months at this point, and I haven't picked a project to wrangle into the spotlight on the home page.

Thanks for reminding me to plug away at it some more :) Not a frontend person at all so this is a labor of love

https://www.markusde.ca/

Respectfully I disagree. Machines with heap are not the only model of computation, and the fact that useful software has been written in python suffices to prove this.

I mean... are we to throw away all code in numerical methods because the canonical, automatic memory management is good enough for most professionals?

They're a good tool for sure, but I take issue with your characterization. It's not "laziness" or "lack of understanding" that makes them ill-suited for python, but just that they're too expressive for the goals python seeks to fulfill.

I suspect that people's aversion to manual memory management is more an expression of that semantic mismatch rather than some kind of reveling in their own stupidity.

You're generalizing so that you can dismiss my argument, though it is probably my fault for being unclear.

When you "just ask questions" on a public platform you implicitly give credence the side with less acceptance. This is fine with issues that are undecided or harmless, but trans personhood is neither. If you agree that trans rights are human rights, and are aware of the trans suicidality rates alongside the latest push of anti-trans legislation in the States and Europe, then it should be apparent that Netflix did not use their large platform responsibly here.

I'm not worried about the trans kid who clicks off of a C-tier netflix special after 20 minutes. They'll be fine. I'm concerned about their uninformed schoolmates, or their school board, or their parents, who get the impression that the personhood of trans people is some disputed academic issue which they are fine to have a "trans-exclusionary" stance on.

Tech companies are poorly positioned to engage in responsible platforming, and pressuring them when they misstep is important.

Stopping shouting != silence.

This is a naive take. Should every minority opinion be given the front page of netflix, regardless of the harm pushing it might leave in it's wake? Or just TERFs?

Anti-trans violence and suicidality is a major issue and speech around it needs to be cognizant of that. At best in his special Chappelle does a poor job of recognizing this be it because he is maligned, uninformed, or just unclear; Advocating that we should continue amplifying it's message as some insular censorship issue is utterly silly.

This thread is already full of people who didn't read or understand the critique of Netflix as presented in the article. It's not an issue of "Dave Chappelle thinks a bad thing and should be punished" it's "Netflix promotes an equivocation that actively harms people".

> “This is not an argument with two sides. It is an argument with trans people who want to be alive and people who don’t want us to be,” Field added. “This all gets brushed off as offense though — because if we’re just ‘too sensitive’ then it is easy to ignore us.”

Went into the special before it hit the news because I like some of Chappelle's other work. I liked a few parts, and I didn't like others. I think it's totally super neato that Dave Chappelle has his personal opinions on trans people, but publicly playing the "just asking questions" game costs putting giving both sides on equal footing beforehand.

This is an irresponsible thing of Netflix to do, and silly to conflate with censorship. Yelling "I think there's a fire" in a crowded building causes as much harm as yelling "are we sure the building's really burning?" when it is. Absolutely think and say either if you want to, but know that when you amplify them it causes real social harm.