My path to this subject was tortured, so sorry if I don’t account for Polysemy etc.

With Prop, I think what you need to dig into is ‘non-computational’ not ‘non-computable’.

Mere propositions is probably best viewed with Homotopy Type Theory[0]

Two proofs (t1,t2) of the same proposition (p:Prop) which are definitionally equal are proof irrelevant, meaning that all they carry is the proof p is true.

This paper [1] may be helpful but the difference between groupoids and subsingletons with classical mathematics is challenging for many of us.

Hopefully this helps in your journey.

Also remember that with classical set theory the internal and external proposition truths are different, the Curry–Howard correspondence is to constructivist from lambda calculus, you don’t have PEM etc…

Remember DGM[2] shows that finite indexing or projection is PEM

Good luck and I hope you continue to share your journey.

[0] https://homotopytypetheory.org/wp-content/uploads/2013/03/ho...

[1] https://jesper.sikanda.be/files/definitional-proof-irrelevan...

[2] https://ncatlab.org/nlab/show/Diaconescu-Goodman-Myhill+theo...

1) rfl vs doing a proof:

It depends on how your things are defined. For example, consider the function that appends two lists, a classic in functional programming (Here's a refresher: https://stackoverflow.com/a/35442915/2694054 )This is usually defined by recursion. But the details matter: The example in the link is defined by recursion on the first argument. That is, for a concrete first argument, it can evaluate. So it can e.g. evaluate `append [] ys` to `ys` just by unfolding the definition and resolving matches. But for `append xs []` you can not evaluate the `xs` any further because the remaining behavior depends on its concrete shape. So to prove that `append xs [] = xs` you need a proof (by induction).

2) Prop vs Decidable

Prop is a mathematical proposition. For example, the Riemann Hypothesis is a Prop. But a decidable Proposition is one for which you can write a program that knows if it is true or false. And you need to actually write this program, and prove it correct. So currently the Riemann Hypothesis is not decidable, because no one figured out how to write that program yet. (It will be a simple `return true` or `return false`, but which??) This mostly shows up for something like `forall x y, decidable (x = y)` which allows you to say that for any two numbers you can decide if they are equal or not. You can then use this when you actually do functional programming in Lean and actually want to run the program on concrete inputs.

The remaining two questions are more specific to Lean's engineering so I won't even attempt to answer that.