should I formalize WASM instead?

Stream: new members

[Huỳnh Trần Khanh]

I'm trying to reason about competitive programming programs. I can't directly express the algorithms in Lean because the limited semantics make it hard to express memory reuse and other tricks that make the programs efficient. My original idea was to formalize a restricted subset of C++, however after a while I realized that this might be overkill. Is it a good idea to use WASM as a language to express imperative algorithms?

[Huỳnh Trần Khanh]

If you don't know what competitive programming is, this page is full of competitive problems: https://cses.fi/problemset/list/. The https://usaco.guide page also provides a good introduction.

[Yakov Pechersky]

How about LLVM?

[Huỳnh Trần Khanh]

Ease of formalization should also be considered, LOL. LLVM IR is a humongous language.

[Huỳnh Trần Khanh]

Competitive programming programs don't do much I/O aside from reading and writing to standard streams.

[Huỳnh Trần Khanh]

So far, WASM seems like a promising candidate but I want experts to weigh in too.

[Mario Carneiro]

Why not formalize IMP or lisp instead? Something semi-practical but with a small basis so you can prove properties

[Mario Carneiro]

almost any real world language will have way too many moving parts for your needs