I’m uncertain about what R abstractions/models are best to use for reasoning about AI. Coq has a numberofoptions, which might imply different things about provability of different propositions and economic viability of those proofs getting anywhere near prod. Ought a type theorist or proof engineer concern themselves with IEEE754 edge cases?
We are not at the stage of formal verification, we are merely at the stage of constructing a theory from which we might be able to derive verifiable specifications. Once we have such specifications we can start discussing the engineering problem of formally verifying them. But the latter is just the icing on the cake, so to speak.
I’m uncertain about what R abstractions/models are best to use for reasoning about AI. Coq has a number of options, which might imply different things about provability of different propositions and economic viability of those proofs getting anywhere near prod. Ought a type theorist or proof engineer concern themselves with IEEE754 edge cases?
We are not at the stage of formal verification, we are merely at the stage of constructing a theory from which we might be able to derive verifiable specifications. Once we have such specifications we can start discussing the engineering problem of formally verifying them. But the latter is just the icing on the cake, so to speak.
I personally think work on reduced precision inference (e.g. 4 bit!) is probably useful, as circuits should be easier to analyze than floats.