Post #4138471
2026-07-27 13:56 UTC
"We have proof automation now": https://www.imperialviolet.org/2026/07/26/zstd-lean.html
In which someone who's terrible at using interactive theorem provers wonders whether dependently-typed languages might be interesting now that the machines can easily write the proofs for you. Also there's zstd involved.
Replies (2)
-
@jfdm@discuss.systems 2026-07-27 14:08
@agl@infosec.exchange To be frank, dependently-typed languages have always been interesting and we have had the machine help us write the code long before GenAI/LLMs became 'de jour'. The devil appears with writing your initial theorems not when asking the machines to provide proofs. The old mantra still exists: Garbage in; Garbage out. Bad propositions in; Bad proofs out.
-
@shriramk@mastodon.social 2026-07-27 14:08
@agl@infosec.exchange Oh, I thought this was a flame (which would be much more on brand for Mastodon), then realized you're the author of the blog post. (-: