CS Researchers: Here're some programming languages mathematically proven to make the computer do exactly what you say.

Programmers: «create vast complexity that no one person could comprehend in order to render a web page»

Also Programmers: What if we made the programming language English, required that the compiler run on a monstrously huge array of GPUs, and set it up so it only did what we ask sometimes, and other times just do nonsense, but we don't know which is which?

Hacker News: Neat!

@davetron5000 in conclusion, computers are a land of contrasts.
@davetron5000 out of curiosity what are these languages cs researchers are making?

@hawkticehurst @davetron5000 If you're interested in writing programs that are "mathematically proven to do exactly what you say" take a look at "dependently typed" programming languages like Idris (also agda, coq, f*, and lean, though those seem more focused on theorems proving than programming).

And the topic of "formal verification" in general.

@davetron5000 Also programmers: Now let’s shove it into every screen under the sun.
@davetron5000 @hamza those are managers and executives, not programmers