Posted by signa11 14 hours ago
fn sin(x: f16) -> f16
There are only 64k different f16s. Easy enough to test them all. A given sin() is either correct or it's not.Yet sin() here can have a large number of different implementations. The spec alone under-determines the actual code.
If "spec" doesn't imply that, what does it mean to you? Or maybe you are suggesting that C "code" isn't code[1] either?
[1] By the original definition of code that is actually quite true, but I think we can agree the term, as normally used, has evolved over the years?
To invert your polynomial analogy, the specification might call for a sine wave, your code will generate a Taylor series approximation that is computable.
Simply put: Formal language = No ambiguities.
Once you remove all ambiguous information from an informal spec, that, whatever remains, automatically becomes a formal description.