Formalization of algorithms?

Stream: Is there code for X?

[Jihoon Hyun]

This just came to my mind, and I wonder if there is some discussion about this.
My intuition says we would first have to define an architecture, like Von Neumann Architecture, then define some basic instructions (including concurrent instructions) which are O(1), and finally define algorithm as a finite list of instructions.

[Mario Carneiro]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Computational.20Complexity.20Theory