A Very Small SAT Solver (From Haskell) Now in Dafny, Proved Correct with LLMs | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		A Very Small SAT Solver (From Haskell) Now in Dafny, Proved Correct with LLMs (github.com/namin)
		4 points by namin 3 months ago \| hide \| past \| favorite \| 2 comments

vdupras 3 months ago [–]

I asked the LLM whether my program was correct and it answered: you're absolutely right!

namin 3 months ago | [–]

Ha. At least you can check the theorem statements and see that the proofs verify :)

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact