Hacker News: rafaelRiv

New comment by rafaelRiv in "We have proof automation now"

rafaelRiv — Mon, 27 Jul 2026 15:55:38 +0000

I do but I have no guarantee that the llms will make a sane implementation of the types

New comment by rafaelRiv in "We have proof automation now"

rafaelRiv — Mon, 27 Jul 2026 13:18:31 +0000

I program very often in idris2 and I cannot agree more. LLMs tend to take the least effort possible to the point where most of the time, llms are just not useful to program with dependent types. At least, not yet

New comment by rafaelRiv in "We have proof automation now"

rafaelRiv — Mon, 27 Jul 2026 12:47:55 +0000

I would say that the value of dependent types in software engineering isn't in proving all code correctness. As a user pointed out in the idris2 Zulip, most programs using dependent types don't have, and shouldn't have, proof of validity for the entire program. Instead, you simply get more correct code by construction, and I think that's the whole point.

I'm currently developing a unikernel in idris2, and the experience is very pleasant (unfortunately, I'm not quite ready to share it yet).

New comment by rafaelRiv in "The LLM Critics Are Right. I Use LLMs Anyway"

rafaelRiv — Sat, 18 Jul 2026 17:22:32 +0000

As if programming by hand was sooooooo inconvenient

New comment by rafaelRiv in "The LLM Critics Are Right. I Use LLMs Anyway"

rafaelRiv — Sat, 18 Jul 2026 17:17:33 +0000

Jesus ! You guys are very authoritharian. Even if it is now the norm, I prefer to not use that tool and I bet the more the time past and the more I will be faster than anyone that use LLMs (because of skills atrophy)

New comment by rafaelRiv in "The LLM Critics Are Right. I Use LLMs Anyway"

rafaelRiv — Sat, 18 Jul 2026 17:10:26 +0000

What is your metric ? How do you calculate ROI ? Strange that you didn't specify that. Also, are you sure your "25% increase" is due to LLMs ? Every time I see this claim, it is always for a short time period or the increase was not due to LLMs at all

New comment by rafaelRiv in "The LLM Critics Are Right. I Use LLMs Anyway"

rafaelRiv — Sat, 18 Jul 2026 17:01:17 +0000

LLMs are not deterministic and I still look at compiler result and I encourage people to look at it. That people don't look at the result of compiler is a problem and not a an argument

New comment by rafaelRiv in "After 7 years in production, Scarf has reluctantly moved away from Haskell"

rafaelRiv — Sat, 18 Jul 2026 02:08:23 +0000

And you are being authoritarian by telling us which tools we should use for our careers. At this point, llms have give me more work than anything else