Here is a piece of the Arm-A ASL:

    (result, -) = AddWithCarry(operand1, imm, '0');
    if d == 31 then
      SP[] = ZeroExtend(result, 64);
    else
      X[d, datasize] = result;

and here is some analogous Sail (automatically translated from the ASL, in fact):

    (result, nzcv) = AddWithCarry(operand1, operand2, carry_in);
    if d == 31 then {
        SP_set() = ZeroExtend(result, 64)
    } else {
        X_set(d, datasize) = result
    }

I'm somewhat at a loss to understand in what way that's less readable?

(There surely are things that can be improved, of course - e.g. perhaps the concrete syntax for fancy types - but readability was a primary goal in the Sail design; it's really not a theorem-proving language or something that needs fancy PL knowledge.)