Hacker News

Top stories

Live mirror
30 storiesupdated just nowView source snapshot
  1. F-Droid 2.0 (f-droid.org)
    280comments
  2. Show HN: Make cursed fonts like Times New Bastard (mitpit.com)
    79comments
  3. Show HN: Whiteboard (YC W26) – An open-source IDE for thoughtful software design (github.com/devdotfast)
    92comments
  4. Why is the liver so weirdly regenerative? (dynomight.substack.com)
    170comments
  5. 2DWillNeverDie (2dwillneverdie.com)
    21comments
  6. Fearless SIMD v1.0 (linebender.org)
    33comments
  7. Rails World 2026 Opening Keynote [video] (youtube.com)
    300comments
  8. Toyota is taking the Corolla electric (electrek.co)
    446comments
  9. Using LLMs to trace alchemical knowledge and decode 17th century letters (resobscura.substack.com)
    15comments
  10. My weird new hobby: Wandering around Tokyo on Google Maps (ahmedhossamdev.com)
    110comments
  11. Google’s Project Suncatcher to put ML infrastructure in space (blog.google)
    266comments
  12. Writing Parquet files using Haskell (datahaskell.org)
    3comments
  13. Two-tier encryption in the UK (macanorak.com)
    384comments
  14. Show HN: Air-gapped file encryption as self-decrypting HTML page (apeleg.com)
    16comments
  15. The Board Game of the Alpha Nerds (2014) (grantland.com)
    26comments
  16. Book review: Is parallel programming hard, and, if so, what can you do about it? (ahelwer.ca)
    30comments
  17. California is chasing wealth that has feet (landeconomics.org)
    525comments
  18. Sourcehut account takeover via build logs (XSS in ansi2html) (blog.arusekk.pl)
    14comments
  19. Show HN: Koi.rest – watch some fish and regain your balance (koi.rest)
    38comments
  20. The Bayeux Tapestry: Woven by the Victors (historytoday.com)
    1comments
  21. Security auditing in the age of (good enough) AI (trailofbits.com)
    8comments
  22. The forgotten battle of East Lansing (eastlansinginfo.news)
    15comments
  23. Opus 5.5 is good at explainer videos (launchvideo.io)
    102comments
  24. Forging 1024-bit RSA signatures in nearly SNFS time [pdf] (iacr.org)
    9comments
  25. Geothermal heat map of US hot springs (soakingsprings.com)
    38comments
  26. WaveDigger: Dig into wireless signals to discover their physical locations (github.com/christianrowlands)
    19comments
  27. Stable (YC W20) Is Hiring Product Engineers (usestable.com)
    —discuss
  28. Motor Characterization for Small Running Robots (2016) (robot-daycare.com)
    2comments
  29. Nokia Design Archive (2025) (aalto.fi)
    120comments
  30. Tutoring company tells parents to save their money and 'use AI instead' (afr.com)
    161comments

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.