remywang

Looks like Andy's here, so if you see this - please also try to convince ClickHouse to consider funding DB research in academia. With all the money being poured into AI and the chaos in government funding, there is almost nothing for DB research anymore.

That’s because syntax is the least interesting part of F*.

Isn’t a disproof of the Collatz conjecture easy to check as it should just be a counterexample? Or is the proof not constructive?

Does this work for release builds or just debug builds now?

Does he read his tests and constraints? You’d need lots of tests to have that kind of confidence (SQLite has 500+ lines of tests per line of code), at which point it’s not a lot of additional work to just read the code.

If anyone wants a great mail client, I highly recommend Mailmate which among other things lets you write messages in markdown: https://freron.com/ it’s maintained by a solo dev for 15+ years and charges a fair price

I’ll gladly use AI to write if it were good at writing as much as how it is good at coding. But it’s just a terrible writer, and currently it’s easier to type things out myself compared to yelling at Claude.

Please link to https://developers.google.com/custom-search/v1/overview instead of whatever this is.

It’s time to pull yourself out of your tunnel vision and look at the wasteland left behind by the ruthless machine you are building.

> This will probably prevent git-annex from taking advantage of most new improvements to the Haskell language going forward. That is deeply unfortunate. This is the main reason why git-annex is not guaranteed to never change to depend on LLM generated code, because cutting it off from all future Haskell language improvements may be worse than the alternative.

Looks like they are aware, and git-annex has been around for decades written by one of the best Haskellers. “Some guys hobby project” is not fair

Just stop using that cursed website

Currently the worst assault on open source is PR spam and the collapse of trust and culture that comes with it. Focus on that if you really want to defend open source.

> Telling people “you must read all the code generated by an LLM” is definitely meaningful—but it is not at all moderate (so most people won’t do it)

But they should! The code is the best source of truth on what the software is doing after all.

Instead of giving up on that, we should make it easier to read generated code, e.g. by generating less code in a higher level language.

On the flip side, forcing myself to read all the code also resulted in a smaller, higher quality code base.

I really like my playdate! Lots of indie games, and their Lua API is very good, coming from someone with no prior experience with Lua or games programming.

I had some good fun writing non-gaming apps for the playdate console including a browser [1] and Kagi news mirror [2] and feel the device has great potential as an alternative to android/iOS duopoly

[1]: https://github.com/remysucre/ORBIT

[2]: https://github.com/remysucre/cranky-news

You’re not supposed to use the “brainmade” watermark on an AI generated article.

CPS was also the OG "AI psychosis" when it appeared in Sussman and Steele's AI Memo #349: https://en.wikisource.org/wiki/Scheme:_An_Interpreter_for_Ex...

Select-Project-Join, not Simon Peyton Jones :)

There are fewer foot guns in Prela in particular no NULLs which should help both humans and robots.

Yes, maybe not the language itself, but the ideas behind it. Tarski's Algebra of Relations is actually a better model for modern columns stores than the standard relational algebra, because a column is a binary relation from the primary key into its value.

Claude had no problem translating SQL into Prela, and because you have fine grained control over the query plan (a Prela query is a plan), it was able to optimize queries to be very fast

The best way to understand the theorems is to try to understand the proofs, and the short book “Gödel’s proof” by Nagel and Newman is excellent for that. Just like Douglas Hofstadter wrote in the foreword, I found the book an absolute page turner and finished in one afternoon.

He is not giving advice to the industry, he is giving advice to aspiring programmers and computer scientists. He has no experience in industry, but has produced lots of high quality software and research.

This is exactly domain key normal form!

https://en.wikipedia.org/wiki/Domain-key_normal_form

Here’s the accompanying code on github but we never got to that part in class: https://github.com/nrnrnr/build-prove-compare-student-code

We got to build mini versions of the first 4 languages (imperative, lisp, ML, Smalltalk) in the PL course at tufts which is now published as a textbook [1]. There used to be a prolog part that sadly got cut.

[1]: https://www.cambridge.org/ir/universitypress/subjects/comput...

All of these are supported in pandoc markdown:

> .mdv is strict CommonMark plus four additions:

> YAML front-matter for title, theme, named styles, and dataset references.

> Fenced blocks for data/visuals: ```chart type=bar x=region y=sales.

> ::: containers for styled regions and layout: ::: callout / ::: columns.

> ::: toc for an auto-generated table of contents.

Have a motherfucking website [1] and you’ll be ready for agents or whatever

[1]: https://motherfuckingwebsite.com/

Read manuals to learn niche software, right now I’m reading about LyX and TeXmacs (their manuals are very well written). Lots of these more niche software can always use more love and users.

Anton also wrote the fantastic codapi [1] for embedding executable code snippets with wasm

[1]: https://codapi.org/