Hacker News

Top stories

Live mirror
30 storiesupdated just nowView source snapshot
  1. F-Droid 2.0 (f-droid.org)
    239comments
  2. Show HN: Koi.rest – watch some fish and regain your balance (koi.rest)
    17comments
  3. Show HN: Make cursed fonts like Times New Bastard (mitpit.com)
    57comments
  4. California is chasing wealth that has feet (landeconomics.org)
    213comments
  5. Show HN: Whiteboard (YC W26) – An open-source IDE for thoughtful software design (github.com/devdotfast)
    72comments
  6. Why is the liver so weirdly regenerative? (dynomight.substack.com)
    129comments
  7. Fearless SIMD v1.0 (linebender.org)
    27comments
  8. 2DWillNeverDie (2dwillneverdie.com)
    4comments
  9. GitLab Outage (status.gitlab.com)
    4comments
  10. Rails World 2026 Opening Keynote [video] (youtube.com)
    216comments
  11. My weird new hobby: Wandering around Tokyo on Google Maps (ahmedhossamdev.com)
    76comments
  12. Back and shoulder surgery is often worse than useless (economist.com)
    4comments
  13. Using LLMs to trace alchemical knowledge and decode 17th century letters (resobscura.substack.com)
    9comments
  14. International observers to investigate Swedish election fraud (tv4.se)
    8comments
  15. Toyota is taking the Corolla electric (electrek.co)
    238comments
  16. Stable (YC W20) Is Hiring Product Engineers (usestable.com)
    —discuss
  17. The Board Game of the Alpha Nerds (2014) (grantland.com)
    17comments
  18. Google’s Project Suncatcher to put ML infrastructure in space (blog.google)
    144comments
  19. Book review: Is parallel programming hard, and, if so, what can you do about it? (ahelwer.ca)
    22comments
  20. Sourcehut account takeover via build logs (XSS in ansi2html) (blog.arusekk.pl)
    8comments
  21. Security auditing in the age of (good enough) AI (trailofbits.com)
    2comments
  22. Two-tier encryption in the UK (macanorak.com)
    370comments
  23. Forging 1024-bit RSA signatures in nearly SNFS time [pdf] (iacr.org)
    6comments
  24. The forgotten battle of East Lansing (eastlansinginfo.news)
    12comments
  25. Geothermal heat map of US hot springs (soakingsprings.com)
    30comments
  26. Early rogue AI agent activity and attempts to hack found on urlquery.net (transluce.org)
    216comments
  27. WaveDigger: Dig into wireless signals to discover their physical locations (github.com/christianrowlands)
    14comments
  28. Tutoring company tells parents to save their money and 'use AI instead' (afr.com)
    108comments
  29. Opus 5.5 is good at explainer videos (launchvideo.io)
    72comments
  30. Show HN: AgentRun: DSL to turn agents into workflows (github.com/parcha-ai)
    6comments

Prediction: AI will make formal verification go mainstream

10 pointsby 9mo agomartin.kleppmann.com
2 comments
9mo agoHN ↗

What a grim future, just chat with a bot without ever seeing the code

9mo agoHN ↗

This is what's going to happen:

- Formally verifiable specs improve the absolute garbage that is LLM generated code to an acceptable degree.

- Realization: Providing formally verifiable specifications is actually a lot of work

- Light bulb: Oh, let's have the LLM generate formal specifications.

- Realization: Oh, actually those autogenerated specifications aren't correct

- Conclusion: We're back to square one.

There is a reason why most code is not formally verified. It's actually really hard (and in many cases arguably not worth it) to express what one would call "standard business logic" in formally verifiable terms.