Clarification of Skepticism

[Timothy Y. Chow]

Freek Wiedijk wrote:

> I agree with Harvey that you really would like a system in which 
> experimenting with data, graphing and making diagrams, _and_ 
> representing the definitions, statements and proofs is all together. 
> Currently we have systems like Mathematica on the one hand, and the 
> proof assistants on the other hand, and they are not close to merging 
> yet. (I once had a project to work towards this goal -- it was called 
> FEAR, formalising elementary analysis rigorously -- but that 
> unfortunately never went beyond a prototype stage.)

Another prototype worth mentioning was created by Muhammad Taimoor Khan 
for his 2014 doctoral dissertation, "Formal specification and verification 
of computer algebra software":

https://www3.risc.jku.at/publications/download/risc_4981/main.pdf

Tim