Hacker News new | past | comments | ask | show | jobs | submit login

> AFAIK, the only languages that fully express the com meaning formally with types are the dependently typed ones.

I said “formally”, not “with types”. I firmly believe in using the right tool for the job, and some things are best handled with manual proofs. As helpful as types might be for computer-generated proofs (type inference), I'd rather carry out my manual proofs using good old-fashioned predicate logic. Some proof techniques still need to be backed up by type structure, though (e.g., induction over datatypes).

> Every other program in every other languages has most of its meaning expressed informally, in the mind of the programmer.

Unfortunately, I can't read minds. I can only read proofs that have been explicitly written down.

> Unless you believe that no programs work, then nearly all programs that do express most of their meaning informally.

My definition of “work” is “works in all cases”. No bugs. No unforeseen cases.




So you're specifying an empty set. There has never been a large program that's been completely formally proven -- not a single one -- and there are therefore no methods that work. The small programs that have been mostly proven, took such a great effort, that their creators wouldn't say that the approach "works" in any widely applicable way.


Yep, that's the state of the art. It means that more human work has to be done on making it easier to write programs that work.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: