Minimal subset of Ecmascript to formalize and use...

Stream: new members

[Ilmārs Cīrulis]

I'm thinking about writing Javascript that's proven correct and using in tiny Javascript "programs" on my static website. But I don't care about many parts of it.

For example, not interested in floating point numbers or limited size whole numbers that come by default, only in integer numbers (bigints) and rational numbers (basically pair of two bigints). What else could be thrown away? Of course, basic data types and operations, functions and basic objects (interpreted as dictionaries?), also arrays are here to stay, for sure.

What's your opinion about this weird idea - to formalize this minimized part of Ecmascript in Lean and then use?

[Ilmārs Cīrulis]

(This is daydreaming for now, but why not?)

[Ilmārs Cīrulis]

Btw, does Lean have something like a program extraction (like Rocq Prover does - it can, I believe, be used for extraction of source in Ocaml, Haskell and some kind of third language)?

[Ilmārs Cīrulis]

Right now looking at this (old) formalization of Ecmascript subset (https://blog.brownplt.org/2012/06/04/lambdajs-coq.html) and thinking of "stealing" some part of it for my purposes.

[Will Bradley]

This includes a Lean 4 runtime in WebAssembly, so that could be a good starting place. I haven't used it though. You might also want to reach out to @/cognivore, the developer

[Ilmārs Cīrulis]

Here we go with the first things:

inductive Constant where
| number: ℤ → Constant
| string: String → Constant
| boolean: Bool → Constant
| undefined: Constant

mutual
  inductive Value: Type where
  | const: Constant → Value
  | function: ℕ → Expression → Value
  | object: List (String × Value) → Value
  | array: List Value → Value

  inductive Expression where
  | var: ℕ → Expression
  | val: Value → Expression
  | assign: ℕ → Expression → Expression → Expression
  | fun_apply: Expression → List Expression → Expression
  | getter: Expression → Expression → Expression
  | setter: Expression → Expression → Expression → Expression
  | delete: Expression → Expression → Expression
  | array_get: Expression → Expression → Expression
  | array_set: Expression → Expression → Expression → Expression
  | if_then_else: Expression → Expression → Expression → Expression
  | while_loop: Expression → Expression → Expression
  | error: String → Expression
  | done: Value → Expression
-- primitive operations of integers
  | int_addition: Expression → Expression → Expression
  | int_subtraction: Expression → Expression → Expression
  | int_multiplication: Expression → Expression → Expression
  | int_division: Expression → Expression → Expression
  | int_remainder: Expression → Expression → Expression
  | int_power: Expression → Expression → Expression
  | int_opposite: Expression → Expression
  | int_lt: Expression → Expression → Expression
  | int_le: Expression → Expression → Expression
  | int_eq: Expression → Expression → Expression
  | int_ne: Expression → Expression → Expression
end

[Ilmārs Cīrulis]

This stuff is very hard to even think about, ugh. :O

[Ilmārs Cīrulis]

Function is thing with natural number n of parameters and body, which is expression with those specific parameters unbounded, right? Like in this definition above.

Maybe I should change the function: ℕ → Expression → Value to something like function: List ℕ → Expression → Value. And maybe add some inductive predicate like, dunno, wellformed for Expressions... :thinking:

[Ilmārs Cīrulis]

Ok, it seems I have settled on inductive definitions for AST. This version looks better, imo.
Took "inspiration" from https://github.com/querycert/jsast (suggested on Rocq zulip chat).

inductive UnaryOp: Type where
| opposite
| negation

inductive BinaryOp: Type where
| multiplication
| division
| remainder
| addition
| subtraction
| lt
| le
| eq
| ne
| and
| or
| has_property
| get_property
| set_property
| delete_property
| array_get
| array_set

inductive Literal: Type where
| null
| undefined
| boolean: Bool → Literal
| string: String → Literal
| integer: ℤ → Literal

mutual
  inductive Expr: Type where
  | identifier: String → Expr
  | literal: Literal → Expr
  | object: List (String × Expr) → Expr
  | array: List Expr → Expr
  | function: List String → List Stat → Expr
  | fun_apply: Expr → List Expr → Expr
  | unary_op: UnaryOp → Expr → Expr
  | binary_op: BinaryOp → Expr → Expr
  | if_then_else: Expr → Expr → Expr → Expr
  | assignment: Expr → Expr → Expr

  inductive Stat: Type where
  | expr: Expr → Stat
  | block: List Stat → Stat
  | var_decl: String → Option Expr → Stat
  | conditional: Expr → Stat → Option Stat → Stat
  | while: Expr → Stat → Stat
  | fun_return: Option Expr → Stat
  | error: Expr → Stat
end

[Ilmārs Cīrulis]

Now going to read publications from here and cry (probably). :D

[Ilmārs Cīrulis]

I'm too stupid or maybe lazy (or both)...

How much would it cost if I want to pay someone to formalize the semantics (?, is this the correct word)? To make AST executable and possible to reason about results of execution?

I have 400-500 euros saved. Probably this number must be multiplied by 10, at least... :joy: :sweat_smile:

[Ilmārs Cīrulis]

Maybe I should use my miserliness as motivation to learn necessary stuff...

[Ruben Van de Velde]

I'm afraid that would be several orders of magnitude short :)

[Ilmārs Cīrulis]

Aha, got it. Must be multiplied by 100, at least. :D

[Ilmārs Cīrulis]

At least I don't want all Ecmascript. :) That saves some expenses to me.

[Ilmārs Cīrulis]

Maybe there's some good book for beginner like me? Let's go googling.

[Ilmārs Cīrulis]

1) http://concrete-semantics.org/ - this will be first step
2) Robert Harper's "Practical Foundations for Programming Languages" - as something to study after the first step is done

[Ilmārs Cīrulis]

Should be good plan

[Mario Carneiro]

it's probably a better idea to get someone else to pay you to do it

[Eric Wieser]

You might have a better time trying to formalize webassembly

[Eric Wieser]

Oh, I see someone already made a runtime linked upthread. You could probably try to prove things about very small webassembly programs using that.

[suhr]

1. You can verify safe Rust programs with https://github.com/creusot-rs/creusot
2. A rust program can be compiled into webassembly
3. ??????
4. PROFIT

JS is not a good language for formal verification, it's not even typed.

[suhr]

I think you also can compile Ada/SPARK to wasm.