Your link is very interesting - but it also makes it quite clear why there are not yet any commercial applications of it.But then, we have to assume that AI will make the work of development easier, probably geometrically easier, over time. So maybe in five years or so, it could become SOP.
I can’t help contrasting the painstaking formal process of writing to provable safety, on the one hand, with the FORTRAN code for the Climate-change models whose outputs we are told to trust implicitly and stake our grandchildren’s futures on. Code with comments in it making clear that it was written by people who didn’t trust it themselves - but who were under direction to “just do it.”
Thank you; I find the work in provability/formal-methods to be quite interesting.
but it also makes it quite clear why there are not yet any commercial applications of it.
True — But it also shows that it's (a) feasible, and (b) a matter of time/effort/money.
But then, we have to assume that AI will make the work of development easier, probably geometrically easier, over time. So maybe in five years or so, it could become SOP.
True AI? That's a long, long way off.
Last I'd heard we're pretty much at the level of epileptic chicken
.
This is a bit different: automated and semi-automated theorem provers are in a much easier category than true AI.
I can’t help contrasting the painstaking formal process of writing to provable safety, on the one hand, with the FORTRAN code for the Climate-change models whose outputs we are told to trust implicitly and stake our grandchildren’s futures on. Code with comments in it making clear that it was written by people who didn’t trust it themselves - but who were under direction to “just do it.”
True; just because the internal-logic is consistent (or even proven valid) doesn't mean that the output is truthful — for example, if you put give a fuel-consumption calculator a weight that is 10,000 lbs off, you're not going to get an accurate measure.