LightMachine

29 ms·

31.
by LightMachine 9d ago
I'll try to sanitize the commit history, I had no idea it would be so important
32.
by LightMachine 9d ago
You can prove infinitely many cases by induction. It works like this: if you prove that a property about natural numbers holds for 0, and if you also prove that, assuming the property holds for N, it also holds for N+1; then, you can conclu
33.
by LightMachine 9d ago
Problem is the stdlib is very small so proving even simple theorems still takes a lot more effort (for the AI) than in Lean. We need a mathlib!
34.
by LightMachine 9d ago
It didn't "need to", it just evolves by rewrites as I learn (the project is fairly small) so in the latest rewrite I choose Bend!
35.
by LightMachine 9d ago
obrigado amg
36.
by LightMachine 9d ago
alright, we could try to restore history removing sensitive bits if that's so important. thanks for the feedback
37.
by LightMachine 9d ago
Bend might reply with "Flag is wall".
38.
by LightMachine 9d ago
Yeah, you want to at least read what the AI is putting on LAWS.bend. It is substantially smaller than the codebase. Ultimately LAWS.bend makes you need to read astronomically less code. Not zero code.
39.
by LightMachine 9d ago
Surprise - HVM has been reimplemented in Bend 2. You can find it on Bend's demo directory in our GitHub. Don't tell anyone though!
40.
by LightMachine 9d ago
Hi. Yes and of course, I plan to invest in everything that makes Bend better. The language is, in theory, capable of parallelizing perfectly in any setup. Currently, though, only a very simple scheduler is shipped, and you must still tune i
41.
by LightMachine 9d ago
Exactly, "you can't win" is grossly under-specified. The goal of the demo is just to show that laws can't be broken. Yet, if that's your only law, the AI can do whatever to protect it - including changing how the ch
42.
by LightMachine 9d ago
There isn't a single book that covers all of it... Bend's theory touches various domains (dependent types, substructural types, termination). And then there's the runtime, compiler, GPU kernels... If you mean about the type t
43.
by LightMachine 9d ago
I will improve that phrasing, thanks. It just means that Bend compiles to a single .c file, and that file compiles to either Metal or CUDA, via macros, depending on your target. This shouldn't be relevant to most users. It is just a wa
44.
by LightMachine 9d ago
The check is happening in between the animations. When the AI edits the code, Bend will check if all laws still hold, mathematically so. If not, the AI repeats, until that's the case. So, the animations just show what happens to the ap
45.
by LightMachine 9d ago
There is just a lot of private data and even proprietary code (like SupGen) in the commit story, so I just squashed it. I didn't think that'd be an issue? Why?
46.
by LightMachine 9d ago
Nothing wrong with addressing it conceptually! We will, in the upcoming versions, probably via codata / coroutines. For V1, I'm keeping the language set smell. When it is stable, we'll add more features. Lean had 10+ years to
47.
by LightMachine 9d ago
Yes, there's a lot of vibe-coding in many places, but the critical parts (compiler, runtime, kernel) are human designed, and the kernel has been extensively audited by human. All of it is my own design and architecture, and I'm a
48.
by LightMachine 9d ago
the compiler is in comp.ts, alongside the runtime it is not a pretty file and it has a lot of gambiarra and AI slop for now if you want to read something worthy, read the kernel (bend.ts)
49.
by LightMachine 9d ago
yes, there's a lot of personal info and AI slop in the commit history. is this a problem to you? why
50.
by LightMachine 9d ago
true
51.
by LightMachine 9d ago
Hi, I'm the author. HN staff: someone posted before me. Could we change the title to "Bend - a language that blocks AI mistakes via proof and runs on GPUs"? Everyone: feel free to ask any question, but I'd be highly app
52.
OptMem: Plug-and-play infinite memory for any agent(github.com)
1 points by LightMachine 2mo ago|3 comments
53.
Claude Plays Pokémon(twitch.tv)
75 points by LightMachine 2y ago|24 comments
54.
Show HN: SupGen, an model-free program synthesizer by examples / dependent types(youtube.com)
21 points by LightMachine 2y ago|9 comments
55.
Optimal context passing with HVM's "pure mutable references"(gist.github.com)
1 points by LightMachine 2y ago|0 comments
56.
HVM3's Optimal Atomic Linker (With Polarization)(gist.github.com)
2 points by LightMachine 2y ago|0 comments
57.
Since Agda->JS is unmaintained, I'm now using Sonnet-3.5 as the compiler(twitter.com)
2 points by LightMachine 2y ago|0 comments
58.
Optimal Evaluation in 1 Minute (or 10 Minutes) (or 10 Years)(gist.github.com)
2 points by LightMachine 2y ago|0 comments
59.
by LightMachine 2y ago
The search space I'm using is that of all functions of a given dependent type. That allows you to make the search space by using a strong enough type. For example, if you search for `Integer -> Integer -> Integer` function, it wi
60.
by LightMachine 2y ago
It will just return the smallest function that passes your tests. It works by enumerating ALL possible functions and running them. Obviously, that naive approach is exponential, so, the entire point is whether we can apply some clever trick

More ›