the_benno

The best source is usually authors' websites. You can find a free copy of just about any modern CS paper by googling its title in quotes with "filetype:pdf".

None of them -- Isabelle is developed at University of Cambridge and TU Munich by academics. The parent commenter seems to have some mistaken notions and assumptions about formal methods and PL research.

You can argue that it's growing and/or promising, but there is absolutely no way that the actual research funding coming out of blockchain-land can hold a candle to the big formal methods labs at major tech firms or traditional academic research funding.

Anders Moeller and Michael Schwartzbach's book [1] on static program analysis is a fantastic resource, with (I think) a great balance of theory and practice. If you want to get really deep into the theory of program analysis, Patrick Cousot just published an incredibly thorough book on abstract interpretation (just got my copy this week, so haven't fully explored enough to have much of an opinion on it as a pedagogical resource)

[1] cs.au.dk/~amoeller/spa

No, I wouldn't say that category theory is a prerequisite for domain theory in general.

I'm most familiar with domain theory from Winskel's "Formal Semantics of Programming Languages" (great book, cited as Win93 in the linked PDF), which has a whole chapter on the subject with no reference to category theory.

If you get deeper into domain theory (e.g. by working through this book) surely some category theory will be useful, but it's not a foundational prereq.

My "wisdom" is that microeconomics is complicated... Hardly a controversial statement. I was being serious about a microecon text, but wikipedia would work just fine too.

I'm not on here to argue with people and it seems you have some sort of ideological bone to pick, so this is going to be my last reply. All the best

Sure: literally everything past the first chapter of any microeconomics textbook. Come on, your position is "it just seems obvious", so I'll just say that it _is_ obvious that economics -- a social science full of interconnected and confounding factors -- is not so simple as "if everyone has 10 more dollars then everyone's cost of living goes up by exactly 10 dollars."

Your meaning was indeed clear but I find your reasoning flawed and the cargo-cult intellectualism... silly and pretentious.

The main flaw, to me, is the 1:1 correspondence you draw between the magnitude of UBI-style benefits and cost of living. That may be true (at least under some simplified/idealized econ101 assumptions) if UBI was the sole source of money in the economy, but that's obviously not the case. The crux of the "UBI doesn't cause spiraling inflation" argument is that UBI accounts for a sufficiently small fraction of total incomes that its benefit (greater spending power for lower incomes, and the downstream economic benefits of that spending) outweighs its nonzero but noncrippling inflationary effect.

That is, though the $10 cash benefit you describe may of course increase COL, it does so by some amount between $0 and $10 that is influenced by all sorts of factors you're glossing over.

What is this gobbledygook? These technical terms have meanings that you clearly either (a) do not understand or (b) are abusing to trick less-educated folks into thinking your political opinions are authoritative and intellectual or whatever.

To an audience that _does_ speak theoretical CS, your sprinkling in of its terminology weakens whatever point you're trying to make and comes off instead as silly and pretentious.

Though it is internally-built, Hack is already open source at https://github.com/facebook/hhvm/.

FB uses a pretty wide array of languages internally -- I don't know if they release statistics publicly, but you can filter/search their open-source projects by language at https://opensource.fb.com/projects/#filter.

This is not how unions work. (source: am union member)

Your claims and arguments are against some imagined shitty union-like thing that does not much resemble an actual union.

because it's not a zero sum game? those union busting talking points keep you focused on your less-fortunate colleagues and and not the obscenely wealthy guy screwing the both of you over.

For what it's worth, here are also [1] the Framework community forum thread about Arch and [2] the Arch wiki page about Framework in case you're interested.

I'm still waiting for mine to arrive (in the next batch) but I plan to install Manjaro when it does, and am cautiously optimistic that it'll be mostly painless.

[1] https://community.frame.work/t/arch-linux-on-the-framework-l... [2] https://wiki.archlinux.org/title/Framework_Laptop

Oh, thanks for the correction and apologies for the inadvertent misinfo.

Your comment sent me reading the HOPL paper about SML -- I think I (based on folklore knowledge/informal conversations) conflate the original development of ML with subsequent development and standardization around SML. All of this was well before my time so it's quite interesting to read about some of the details.

F# is an ML-family language, and ML stands for meta-language -- it was designed for language tools and compilers! Andrew Appel's Modern Compiler Implementation in ML is a great resource for code examples that aren't exactly F#, but will look damn close. The book has also been published with C and Java, if you want side-by-side comparisons

They actually dropped support for diffing and incremental parsing a few months back, when they changed up some internal structures to what they call "precise AST datatypes" (which made diffing quite tricky in the type system).

My impression (from the outside looking in) is that there weren't many people making use of those capabilities, so it wasn't a high priority feature. A bit of a shame, though -- it's a really cool tool and I enjoyed building some things on top of it. I switched to a different front-end, though, when I saw that they had removed those features and all mention of incrementality/differencing from the documentations.

I'd be happy to be wrong about this, if anyone has more up-to-date information about semantic!

The short answer is that it's unsolved in general and just done ad-hoc in practice. I'm working on incremental & demand-driven analysis techniques for my PhD research and currently building essentially what you describe. The state-of-the-art is probably this technique from this year's PLDI [1] -- last I heard they were using a batch parser but planning on integrating with tree-sitter at some point. [1] https://dl.acm.org/doi/10.1145/3453483.3454052

adding some context: used most often in discussion of sports in my experience, e.g. Michael Jordan in Basketball, Wayne Gretzky in Hockey, Babe Ruth in Baseball, etc. Carries connotations not only of being one of the best to ever do it, but also a mythos and aura that influenced/continues to influence others.

"should not be published" is very different from "are not published"

I worked on a research project in undergrad that used Reed-Solomon -- we showed a series of images to users, who would later pick those images out of a set of un-trained images in order to authenticate or access some privileged data, sans encryption. the error-correcting allowed for some degree of misremembering or forgetfulness, as is normal in human image recognition tasks.

The professor later spun up a startup that has since been acquired by Dropbox, but I'm unaware what kind of product they're currently working on.

That incident is the same one referred to in the CACM article and elsewhere throughout this thread.

in many cases you're probably right that mandatory type annotations would improve readability. Taking the rhetorical question very literally, though, there are some times when having it two keystrokes away is very helpful. I often query the type of a large expression (e.g. a partially applied function to remember what argument comes next) or the signature of some module

+1 to this -- good point! It sounds like the legacy project that the parent comment mentioned probably wasn't a "good" project in this respect, though.

This has a number of advantages vs. the `export` syntax used in Grain, too. Being able to look at one `.mli` file for a well-documented public interface is much easier than looking through a source file for what's been exported and what hasn't.

I don't care so much about keywords like `fn` personally; I was referring more to:

- `let` in a statement language (as opposed to let-binding expressions)

- comma-separating patterns (as opposed to using pipes to mimic BNF, also potentially causing confusion vs. tuple/record constructors)

- whitespace rather than semicolons for sequencing (though I'd imagine others might disagree on that front).

Some of that overlaps with Rust, to be sure -- I didn't pick up on those similarities at first.

Most OCaml users I know use emacs with tuareg-mode and merlin (or the equivalent in vim). Once you've got that set up (and it's a breeze these days with opam user-setup) it's super easy to navigate an OCaml code base and access type information on demand.

This is a feature, not a bug -- getting the type of an arbitrary expression is two keystrokes away, but there's no visual clutter from excessive type annotations. And the tooling goes well beyond this one feature.

Working in OCaml without merlin+tuareg feels like having a hand tied behind your back (to me), so I feel your pain. This certainly raises the barrier to entry slightly, but I think it's worth it for the convenience and ergonomics once you're past that initial barrier.

This looks like a cool and interesting project, but some of the syntax choices seem a little... all over the place to me. It seems like it's drawing quite a bit of inspiration from ML-family languages without fully internalizing _why_ things are the way they are there.

Of course, that's all "just syntax" and not the end of the world.

Reason targets a similar use case* but, to me, makes a more sane set of syntactic choices and tradeoffs, while also having access to the whole OCaml ecosystem. I'm not sure why one would reach for Grain over that, though maybe I'm just not the target audience here.

* i.e. developers who want type safety, good inference, a familiar JS-ish syntax, and to target the web

edit: I see now that the compiler is built in Reason -- I'd imagine they've thought about these things and made considered choices on syntax!

Have you tried one? This just isn't true. They taste slightly different, but definitely not "less".

If you do it right -- get a nice crust on there, don't overcook it, toast up some decent buns in butter and use good pickles, cheese, etc. -- it's every bit as flavorful and indulgent as a beef burger. (a decent one at least... you're not going to replicate the best of the best, nor should that really the goal)

100% agree. Beyond & Impossible are alright, but there's an uncanny valley quality to them that can be kind of off-putting (to me).

I've been proselytizing these black bean burgers to anyone who'll listen for a while now -- they nail what you're describing.

https://www.seriouseats.com/the-food-lab-the-best-black-bean...

Except that is explicitly a parody/critique of what Brent Yorgey called the "monad tutorial fallacy": https://byorgey.wordpress.com/2009/01/12/abstraction-intuiti...

This is the post that originally coined that phrase.

Looking at the talks/papers from 1978 is a trip: Grace Hopper gave the keynote, and there were talks by legends like Backus, Naur, Liskov, Kurtz, and McCarthy.

There are transcripts available of all of the talks as well as Q&A sessions and the like -- really fascinating to look back on now with the benefit of hindsight.

For example, McCarthy was asked [1] whether he believed "that LISP has made any long-lasting contributions to the more 'normal' programming languages, e.g., FORTRAN and ALGOL, COBOL, etc."

He responded that, yes, he thought conditional expressions and recursion were here to stay. Safe to say he was right about that!

[1] https://dl.acm.org/doi/pdf/10.1145/800025.1198363