Re: formal verification, I wonder if FAI developers will ultimately end up having to resort to improved programming environments to reduce bug rates, as described by DJB:
For more than a decade I have been systematically identifying error-prone programming habits—by reviewing the literature, by analyzing other people’s mistakes, and by analyzing my own mistakes—and redesigning my programming environment to eliminate those habits. For example, “escape” mechanisms, such as backslashes in various network protocols and % in printf, are error-prone: it’s too easy to feed “normal” strings to those functions and forget about the escape mechanism.1 I switched long ago to explicit tagging of “normal” strings; the resulting APIs are wordy but no longer error-prone. The combined result of many such changes has been a drastic reduction in my own error rate.
...
Bug-elimination research, like other user-interface research, is highly non- mathematical. The goal is to have users, in this case programmers, make as few mistakes as possible in achieving their desired effects. We don’t have any way to model this—to model human psychology—except by experiment. We can’t even recognize mistakes without a human’s help. (If you can write a program to recognize a class of mistakes, great—we’ll incorporate your program into the user interface, eliminating those mistakes—but we still won’t be able to recognize the remaining mistakes.) I’ve seen many mathematicians bothered by this lack of formalization; they ask nonsensical questions like “How can you prove that you don’t have any bugs?” So I sneak out of the department, take off my mathematician’s hat, and continue making progress towards the goal.
HT Aaron Swartz. If this approach is taken, it probably makes sense to start developing the padded-wall programming environment with non-FAI test programming tasks well before the development of actual FAI begins, so more classes of bugs can be identified and guarded against. See also.
Such an environment would most likely be based on Haskell, if not something more esoteric.
Assuming performance is a concern, Haskell probably strikes the best balance between crazy-powerful type systems and compiler maturity.
As an anecdote, the exact string-escape issue you’ve mentioned is a (repeatedly) solved problem in that ecosystem, the type system being clever enough to escape most of the verbosity and non-genericity you’d get by trying the same thing in, say, C.
Re: formal verification, I wonder if FAI developers will ultimately end up having to resort to improved programming environments to reduce bug rates, as described by DJB:
HT Aaron Swartz. If this approach is taken, it probably makes sense to start developing the padded-wall programming environment with non-FAI test programming tasks well before the development of actual FAI begins, so more classes of bugs can be identified and guarded against. See also.
Such an environment would most likely be based on Haskell, if not something more esoteric.
Assuming performance is a concern, Haskell probably strikes the best balance between crazy-powerful type systems and compiler maturity.
As an anecdote, the exact string-escape issue you’ve mentioned is a (repeatedly) solved problem in that ecosystem, the type system being clever enough to escape most of the verbosity and non-genericity you’d get by trying the same thing in, say, C.
MIRI has mentioned (for example, in the ‘Recommended Courses’ post) the use of functional programming like Haskell in AI for proof-checking reasons