On the Rectification of Programing Language Spec by Formal Language
0 it's time, for, Xah Edu Corner Extempore! Episode 20161205145300, on the rectification of programing language spec by formal language
1 i've read most of the js spec. let's take a look at this:
2 you see js spec use algorithms as description. lots steps with abstract operations. To understand them, see ECMAScript 2015 §Abstract Operations#sec-abstract-operations
3 using algorithm to describe thing is hard to understand. Like, reading code, and you have to figure out what it's doing, and all side effects.
4 here's example of description by how-to: gcd(a,b)=a, gcd(a,b)=gcd(b, mod(a,b)), mod(a,b)=a-b*floor(a/b). what's gcd?
5 example of description by what-is: gcd(a,b):=n. n := max(S), S ⊂ ℕ, mod(a,n)=0 ∧ mod(b,n)=0
6 the what-is form is much easier to understand than the how-to. Because, reading doc IS to know what-is. Like reading API vs implementation.
7 the what-is is math (including computer science), and how-to is programing.
9 using algorithm as a spec is unfortunate. But using English to do that is worse. JS sec is verbosity multiplied by complexity.
11 if we stick with algorithmic approach to spec, might it possible to replace the English by a program? say #haskell, #ocaml #coq?