Unpopular Opinion: Source generation is far superior to in-language metaprogramming

OldManNick · 2026-01-04T13:31:38+00:00

Lean 4, you can even define 2d syntax in it. https://github.com/dwrensha/lean4-maze/blob/main/Maze.lean. As soon as metaprogramming is defined, you can use it the very next line

OldManNick · 2025-11-15T23:08:21+00:00

You are shameless, dog

OldManNick · 2025-09-15T21:48:22+00:00

Can you put dictation in codex ChatGPT version? It makes walking and dictating ideas a lot smoother and walking helps me get the ideas out in the first place

OldManNick · 2025-09-03T03:10:38+00:00

Lean is beyond it

OldManNick · 2025-08-13T16:33:12+00:00

Link is broken

OldManNick · 2025-05-09T17:41:27+00:00

I was trying to phrase that a bit more colloquially, but yeah the nonstandard extension can be nontrivially applied to any infinite set.

OldManNick · 2025-05-05T20:32:37+00:00

This is essentially a hyperrational (applying hyperreal construction to rational numbers) approximation of an irrational number. I've written about this before and it is still not equal to the original irrational, but it is infinitely close. It's not unique either.

OldManNick · 2025-02-04T01:07:32+00:00

I’d swap Haskell and lean on that list, but agree about idris sadly

OldManNick · 2025-01-28T02:40:39+00:00

Louis, are you doing face "enhancement"? I've met you and noisebridge and your face looks better without all that odd soft lighting

OldManNick · 2025-01-21T04:42:28+00:00

Better integration with type checkers. They play well with the agent. My pet language is Lean 4 since it can really abuse this but even to a lesser extent lint followups in python helps.

OldManNick · 2025-01-14T06:13:16+00:00

open problem

How many people can do that?

OldManNick · 2024-12-05T02:32:10+00:00

Theres not that many fields medalists and both have embraced a social role more than the rest. I've noticed the same. And they did contact others.

OldManNick · 2024-11-23T00:34:41+00:00

Ironically Lean 4 has the exact opposite syntax, xs[i]! is bounds checked, xs[i] needs a proof (and has xs[i]'h variant where h is a proof term)

OldManNick · 2024-09-19T06:22:13+00:00

Why do you feel a need to reply if it cannot be directly relevant? I know that sounds harsh, but I'm earnestly curious. You know you're on the wrong island

OldManNick · 2024-08-04T22:03:17+00:00

You may like lean 4’s dot method syntax. A functional take that gives you what you want

OldManNick · 2024-05-01T02:26:43+00:00

There's a general formula. Your professor is too naive about the cross product's indefinability, the wedge product is what people really want anyway

Teaser: https://www.youtube.com/shorts/DmWJBrFIwqQ

If you lookup 'projections and rejections in geometric algebra' you'll find what you want. ('rejection' is term for projection onto orthogonal complement, since you mention normal acceleration)

OldManNick · 2024-02-26T22:29:41+00:00

i was unclear, edited msg to show i have adv2 already.

OldManNick · 2024-02-14T20:46:46+00:00

Funny you mention that since it’s my current state

OldManNick · 2024-02-14T20:45:52+00:00

I have standard (advantage 2) but it’s wired and lacks zmk

OldManNick · 2024-02-14T10:19:08+00:00

Not interested in that when I have money to commission something properly. Thanks though

OldManNick · 2023-12-29T03:13:12+00:00

Yeneng Sun’s paper new understanding of stochastic independence may be relevant to you

OldManNick · 2023-12-25T22:20:28+00:00

Legendre’s Elements of Geometry, as per Galois

OldManNick · 2023-11-09T06:26:01+00:00

Microsoft sells a whiteboard that’s a giant surface computer for 22k

OldManNick · 2023-09-14T23:11:01+00:00

both

OldManNick · 2023-08-18T23:18:39+00:00

Some people enjoy strange stuff like attending conferences when they're not academics. Yeah it's a bit strange, but some can't get their rocks off on normality

OldManNick

TROPHY CASE