News for hackers. Stuff that matters.

meoleo

meoleo on Hacker News

Re:.md File Is Not a Specification: Using Formal Analysis to Find Requ... on Thursday October 08, 2026 @10:12PM (#50015133)
Do YOU have any case studies or samples built from your specification?
Re:.md File Is Not a Specification: Using Formal Analysis to Find Requ... on Thursday October 08, 2026 @06:53PM (#50013573)
I am not sure if I understand clearly why Kiro's approach would not find the issue.
Re:.md File Is Not a Specification: Using Formal Analysis to Find Requ... on Thursday October 08, 2026 @06:27PM (#50013295)
How is this different from what Kiro does? https://kiro.dev/blog/deep-spec-analysis/
Re:You should write "without bugs" on Saturday January 25, 2025 @05:36PM (#42825614)
TLA+ and Coq are too hard for most SAAS applications. Tried FizzBee (https://fizzbee.io/tutorials/getting-started/) and P (https://p-org.github.io/P/whatisP/)? These seems quite practical.

Coq/Rocq are obviously much harder to use, and I mostly see embedded systems engineers use them. TLA+ is somewhat easier, and being used in a number of cloud infrastructure companies (AWS, MongoDB, Confluent etc).

Obviously, if you are building a simple CRUDL app, these tools don't help at all.