4 ms·
> I'd rather see efficient code generated from a short high level spec This is a holy grail for many PL researchers, but I don't think that there's any languag
by summerlight 6y ago
> I'd rather see efficient code generated from a short high level spec
This is a holy grail for many PL researchers, but I don't think that there's any languages that reached this level of sophistication with expressiveness/practicality enough for production usages. At least with the status quo, you will probably need to write a massive amount of formal proofs if you want logical correctness, even with deceivingly simple specifications.
- chubot 6y agoIt doesn't have to be the same metalanguage for every program. You can write your own code generators adapted to the specific problems. They should have a "pit of success", and the knowledge of the domain is used to ensure that. There are few research-level issues here; it's just good engineering. The 0% or 100% mindset is bad engineering. You want something that's short, and that you can explain to other people, and that other people can write an independent implementation of. If the proof is 10x longer than normal code, and it's written in a metalanguage that the relevant people don't know, then it's not very useful. Proofs are not guarantees. CompCERT has had logic bugs despite being written in a formal language. (It does reduce the number of bugs drastically in general, but it's also an extremely expensive technique, and not what I'm advocating.) There are no guarantees in engineering, just good practices. Groveling through bytes one at a time in imperative languages is not an ideal engineering practice, even if the imperative language comes with more guarantees than most.