On the Rectification of Programing Language Spec by Formal Language

By Xah Lee. Date: . Last updated: .

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:

js spec by algorithm 2017 02 01
ECMAScript 2015 §Indexed Collections#sec-array.from

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.

8 the JavaScript spec takes the approach of how-to (It specify by step-by-step instruction in English). That's unfortunate.

9 using algorithm as a spec is unfortunate. But using English to do that is worse. JS sec is verbosity multiplied by complexity.

10 No human can implement JavaScript by reading the spec alone. I surmise such result would be full of errors.

11 if we stick with algorithmic approach to spec, might it possible to replace the English by a program? say #haskell, #ocaml #coq?

12 if JavaScript spec is done via say formal proof system program, we might actually find all the loopholes in spec of English.