It seems really strange to compare Coq (a functional language for interactive/automatic theorem proving) to plotting tools.