woggy

Well they are much harder to read than tests.

I was going through an experiment trying to spec out a simple caching system in Lean. I was getting Gemini to help me run through doing this, step by step. At one point it writes out this statement with a proof to show something, the specifics of which I forget, but it was some simple property of the cache. I stare at it for a while thinking to myself this can't be right, it was some sort of plain tautological statement that didn't really say anything, like saying 1 = 1.

I give it to Opus 5.5 and it basically confirmed my gut feeling that it was useless.

I'd like to rely more on formal verification. I like the idea of starting out with specs in a formal setting and designing software that way. The problem is it's hard to do right, and my point is even with AI, it's hard to do right.

I found that even with LLMs making sure the formal specification covers what you actually want is challenging.

How do you actually know what the LLM proved is what you want?

Is this Zucks personal AI bot?

I would replace the AI avatars with Daedalus, Icarus, Helios and Morpheus avatars from Deus Ex

Have you guys done any talks or written any articles on how you are developing this software?

Scaling up to this kind of complexity even with AI is still a challenge, at least for me.

I’m curious whether people can use Lean primarily as a software specification language, without necessarily intending to prove everything.

Can we use it to specify module meanings and laws, to make the design precise and checkable, and would allow us to implement property based tests for those laws in our implementation. Lean becomes a tool for more precise thinking about the design.

They should only make these announcements just before releasing. Or at least put a date to it.

I prefer Pro Max Ultra XXL

I can't remember exactly what I did but I think passwords for windows 2000 were stored in something called a SAM file. I managed to get a copy of it and brute force it on my home machine. Password was the schools phone number. Got access to the whole network, network drives, teachers files. I was paranoid so I didn't poke around too much :)

They can keep the buttons and the normal interiors instead of making them look like something out of Star Trek.

Is it that hard? Take a normal car, take engine out, put electric motor in. Don't fuck around with the inside.

Plans for Windows version?

And how lucky Israel allowed and facilitated the transfer of hundreds of millions of dollars to them.

US should mind its own business

"When 1 + 1 + 1 Does Not Equal 3

Consider the number 37. On its own, it is merely data. Say that it represents millions of dollars of investment exposure: that adds context."

Who can even read this? People, please, put some effort into what you publish.