Hacker News Reader

yuppiemephistoon Dispatches from the possibly last days of human relevance

Different Aaronson

yuppiemephistoon All of human cooking compressed into 2 megabytes

Where did you have 10k omakase?

yuppiemephistoon Carbonara Before the Rules [video]

I love the creator Evan. Enthusiasm, intelligence, focus.

yuppiemephistoon A perfectable programming language

some combo of implicit pride and laziness. sorry, i'll fix it up

yuppiemephistoon A perfectable programming language

i agree about this point, i think this is one of the ways extensible syntax can save (or damn, like in this case) you

yuppiemephistoon A perfectable programming language

i was just messing with you guys, but now i'm feeling a bit more motivated

yuppiemephistoon A perfectable programming language

actually i think syntax is incredibly important, but i think i'm approaching it from a viewpoint that's even more syntactic than lisp macros, which in practice tend to center around parens syntactically still. racket a notable exception (and good, but not perfectable lang, one of the inspirations for my remark). typed racket is good but is not culturally central enough. but yeah, i do believe types are [inevitable](https://www.youtube.com/watch?v=0AQdSZqGXz4)

https://reservoir.lean-lang.org/@strata-org/Strata isn't done, but its goal is to let one build whole languages that can look like whatever you like. ones for little kids maybe

syntax matters for normal ppl even more than semantics in some ways since semantics can be optimized and refined on the backend, but everyone is (de)limited by their vocabulary

yuppiemephistoon A perfectable programming language

lean IS that language https://github.com/alok/LeanPlot

yuppiemephistoon A perfectable programming language

https://alok.github.io/assets/lean-position-paper.pdf

i talked about the lisp curse in this old paper. it's rough but explicitly mentions it

yuppiemephistoon We should revisit literate programming in the agent era

I do a form of literate programming for code review to help read AI code. I use [Lean 4](lean-lang.org) and its doc tool [Verso](https://github.com/leanprover/verso/) and have it explain the code through a literate essay. It is integrated with Lean and gets proper typechecking etc which I find helpful.

yuppiemephistoon Parse, Don't Validate and Type-Driven Design in Rust

lean 4

yuppiemephistoon Nanolang: A tiny experimental language designed to be targeted by coding LLMs

Unrelated, but I am literally listening to Rolandskvadet right now and reading your username was a trip

yuppiemephistoon Show HN: Jax-JS, array library in JavaScript targeting WebGPU

This project is an inspiration, I've been working on porting tinygrad to [Lean](github.com/alok/tinygrad)

yuppiemephistoon I ported JustHTML from Python to JavaScript with Codex CLI and GPT-5.2 in hours

I’m doing similar with porting shellcheck Haskell -> Lean

yuppiemephistoon AI will make formal verification go mainstream

There’s 4000 lines of nonstandard analysis which are definitely proofs, including equivalence to the standard definitions.

The frameworks are to improve lean’s programming ecosystem and not just its proving. Metaprogramming is pretty well covered already too, but not ordinary programs.

yuppiemephistoon AI will make formal verification go mainstream

I vibe code extremely extensively with Lean 4, enough to run out 2 claude code $200 accounts api limits every day for a week.

I added LSP support for images to get better feedback loops and opus was able to debug https://github.com/alok/LeanPlot. The entire library was vibe coded by older ai.

It also wrote https://github.com/alok/hexluthor (a hex color syntax highlighting extension that uses lean’s metaprogramming and lsp to show you what color a hex literal is) by using feedback and me saying “keep goign” (yes i misspelled it).

It has serious issues with slop and the limitations of small data, but the rate of progress is really really fast. Opus 4.5 and Gemini were a huge step change.

The language is also improving very fast. not as fast as AI.

The feedback loop is very real even for ordinary programming. The model really resists it though because it’s super hard, but again this is rapidly improving.

I started vibe coding Lean about 3 years ago and I’ve used Lean 3 (which was far worse). It’s my favorite language after churning through idk 30?

A big aspect of being successful with them is not being all or nothing with proofs. It’s very useful to write down properties as executable code and then just not prove them because they still have to type check and fit together and make sense. github.com/lecopivo/scilean is a good example (search “sorry_proof”).

There’s property testing with “plausible” as a nice 80/20 that can be upgraded to full proof at some point.

When the model gets to another jump in capacity, I predict it will emergently design better systems from the feedback needed to prove that they are correct in the first place. Formal Verification has a tendency like optimization to flow through the system in an anti-modular way and if you want to claw modularity back, you have to design it really really well. But ai gives a huge intellectual overhang. Why not let them put their capacity towards making better systems?

Even the documentation system for lean (verso) is (dependently!) typed.

Check out my Lean vibe codes at https://github.com/alok?tab=repositories&q=Lean&type=&langua...

yuppiemephistoon Revisiting "Let's Build a Compiler"

Maybe (vibe) coding it in lean would be fun

yuppiemephistoon Functional Data Structures and Algorithms: a Proof Assistant Approach

https://markushimmel.de/blog/my-first-verified-imperative-pr...

Lean

yuppiemephistoon Racket v9.0

These days, I prefer Lean 4. Its macro system is inspired by racket and it has powerful types

yuppiemephistoon AI is a front for consolidation of resources and power

After reading the article but before seeing this, I adopted that policy. So true.

yuppiemephistoon /dev/null is an ACID compliant database

And the axiom of empty set is an inaccessible cardinal axiom

yuppiemephistoon How has mathematics gotten so abstract?

I like Peano, but he was using Grassmann's definition of natural numbers

yuppiemephistoon Death to type classes

I enjoyed this, hadn't used backpack and this is a nice tutorial

yuppiemephistoon Yet Another TypeSafe and Generic Programming Candidate for C

That’s what I was thinking seeing the username =)

yuppiemephistoon Pony: An actor-model, capabilities-secure, high-performance programming language

Lean 4 truly lets you mathematically reason about code and has metaprogramming that truly makes syntax a surface thing, but if anything people who know this have the taste to want better syntax

yuppiemephistoon Tom Lehrer has died

We sung it at solstice

yuppiemephistoon My first verified imperative program

`show_term grind` and `by grind?` should do what you want

yuppiemephistoon The current state of TLA⁺ development

What do you think of embedding it in a formal system like Lean as a frontend?

yuppiemephistoon How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean

I was surprised to hear their claim about Agda's metaprogramming, I say lean is better here

yuppiemephistoon Show HN: Formalizing Principia Mathematica using Lean

I don’t know about their motivation, but I would say mine is that Lean is a real programming language. Coq is not really meant for “prosaic” programming, more’s the pity.

Lean is also a lot faster.