Hacker News Reader

Comment by devdoomari | Hacker News Reader

um... use dependent types? sorry but I'm from different language background :(

Provable code would solve the root cause, yes. :) However, even with provable code, the proof actually has to be both correct and performed. There are too many competing factors that won't allow idris, for example, to actually work.

The result is that, as an industry, the Internet and the world's business are held together by twine, twist ties, and spaghetti code. Even this very webpage is just enough to work for most people a lot of the time.

so... I guess strong-AI-based coding is the only 100% sure way to go

(but... I'd be jobless if that were to happen :(

Strong AI wouldn't be enough, if by strong AI you mean "enough to pass the Turing test". Humans pass the Turing test all the time, but still produce buggy software.

There are some insanely good architects and programmers. Even so, people write mistaken code, design with faulty assumptions, misinterpret business logic, use libraries and crypto incorrectly, etc. On top of all that, there is a small segment of coders who insert malicious code. They used to write for mayhem but now more for profit.

The terms are somewhat contentious, but AIs are more prone to use heuristics than traditional algorithms, which would add another layer of complexity.

So, we can't be certain that such an AI itself wouldn't create bugs. If anything, it would be easier to show that bugs would get created.

This is simply the state of software. We all deal with it in the ways we can, trying our best to minimize issues and add value.

Or even just QuickCheck? (Hypothesis is an excellent implementation of the concept in Python, so you don't even need Haskell to get the goodness.)

Contracts, like they have in Racket, might also be interesting. They only fail at runtime, but it's easy for mere mortals to express interesting invariants and get good 'blame'.

Reply on news.ycombinator.com