logoalt Hacker News

iFire • today at 4:01 AM • 3 replies • view on HN

I don't use tla+ to model real-world systems anymore, Claude is able to model systems in Lean 4 and the binary executable can handle real input or I can directly generate c / rust on proofs with numeric types that have ring structure (integers, rationals, bits).

https://github.com/lambdaclass/truth_research_zk

Replies

thomasahle • today at 6:34 AM

I'm currently choosing between the right formalization for a big hardware project.

I'm considering between SVA, TLA+ and Lean. With the former being more domain specific and the later more general.

Do you think we'll move towards "Lean for everything" or do domain specific formalisms still make sense?

➕ show 2 replies
dmos62 • today at 7:26 AM

Do you find Lean 4 sufficient for highly async systems?

➕ show 1 reply
dev_arvin2000 • today at 4:11 AM

[flagged]