Yes that's an insightful way of looking at how computer verification could assist in real mathematics research.
Going back to the CS analogy, programmers started out by writing everything in machine language, then gradually people began to write commonly-used functions as libraries that you could just install and forget about (they didn't even have to be in the same language) and they wrote higher-level languages that could automatically compile to machine code. Higher and higher levels of abstraction were recognized and implemented over the years (for implementing things like parsers, data structures, databases, etc.) until we got to modern languages like python and java where programming almost feels like simply writing out your thoughts. There was very little universal coordination in all of this; it just grew out of the needs of various people. No one in 1960 sat down and said, "Ok, let's write python."
until we got to modern languages like python and java where programming almost feels like simply writing out your thoughts. ... No one in 1960 sat down and said, "Ok, let's write python."
For a very good reason: let me invite you to contemplate Python performance on 1960-class hardware.
As to "writing out your thoughts", people did design such a language in 1959...
P.S. Oh, and do your thoughts flow like this..?
public class HelloWorld { public static void main(String[] args) { System.out.println("Hello World"); } }
If it's worth saying, but not worth its own post (even in Discussion), then it goes here.
Notes for future OT posters:
1. Please add the 'open_thread' tag.
2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)
3. Open Threads should be posted in Discussion, and not Main.
4. Open Threads should start on Monday, and end on Sunday.