i love lean4, best in class functional programming language. but i think its "perfectability" is kinda hamstrung by baking non-constructive axioms into the standard library. the kernel has to treat these as opaque constants that cannot be reduced.

i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.

Imo F* is a much better choice for proof-oriented programming than lean4. The latter is still largely about mathematics while the former has things like https://fstarlang.github.io/lowstar/html/LowStar.html

Yes, a strong argument, and staying in a line of PLs: F# for high-level, and F* <-> Low* for theorem proving and low-level coding. I am evaluating F/Low for verified code on Cortex M processor that I am currently trying to write SPARK2014. The Cortex A processor is running seL4 for less safety-critical tasks. I did look at Lean4 as a scratch for my Idris2 itch use cases.

Still working on my LPFM radio station https://www.kpbj.fm/

We have over 60 shows now, rented a studio, and are in talks to security a site for our tower. I'm building out an online store but really need to focus on fundraising.

I actually find Gmail a better editor/grammar check then LLMs. It makes isolated simplifications/corrections that imo have minimal style impact and just focus on clarifying phrasing.

Yeah Gmail got crazy good in the last 3 months, pretty sure it's LLM driven too but it went from 90s MS Word to better than Grammarly recently IMO

I'm not saying we are in one, but isn't a RAM shortage like this is exactly what one would expect at the early stages of a take off scenario?

Same. I've been using the same apple earbuds since like 2005(?). I still have the original plastic case for them and use it to store them in my backpack.

Yes Person of Interest is great! It starts kinda slow as a fairly generic police procedural but gets really epic by the end.

Does it change your perspective on agentic systems like Openclaw?

I keep coming back to Daniel Suarez' breakout novel. It feels so topical with the rise of agentic AI and I often wonder if when and when something like it could arise.

> Haskell is great, for what it's worth, but as with any language you have to reign in the AI's use of excessive verbosity. It will stack abstractions to the moon even for simple projects, and haskell's strengths for humans in this regard are weaknesses for AI - different weaknesses than other languages, but still, TANSTAAFL

I haven't had this problem with Opus 4.5+ and Haskell. In fact, I get the opposite problem and often wish it was more capable of using abstractions.

I guess it might be something with the subject matter and how I'm prompting. I prefer somewhat more imperative haskell though so that's probably a taste thing.

I've been using LLMs (Opus) heavily for writing Haskell, both at work and on personal projects and its shockingly effective.

I wouldn't use it for the galaxy brain libraries or explorations I like to do for my blog but for production Haskell Opus 4.5+ is really good. No other models have been effective for me.