Hacker News

Top stories

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

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.