Save LH-Slack conversation regarding #assume:

[shingarov]

Prof. Jhala's wording makes for an especially elegant explanation of #assume. We don't want to lose it to the non-permanent nature of Slack.

[shingarov]

@janvrany I have a vague recollection that you did a change called something like "Distinguish between assume and assert, even though this is a dummy for now" in one of "your" subsystems? I did a fresh make of latest Tinyrossa (because it pulls in "everything") and browsed for #assume: and #assert: but couldn't find it. Am I hallucinating?

[janvrany]

At the risk of unleashing a wider and opinionated discussion about comments, I'd like informal explanation as well. Not being "on the forefront of formal" myself, I'd find it difficult to unrestand how to use it and what exactly is the difference (now I do, but only after previous eposure to the topic). Especially in this kind of method / API. Something along the lines of:

    "
    “Ensures” a postcondition `aBlock` is met. Confusingly similar to `#assert:`!

    Informally, use `#assume:` in methods to ensure the method is called properly and `#assert:` to 
    ensure invariants during and after method execution. In other words, if `#assume:` fails it is caller's 
    fault whereas when `#assert:` fails it is the method's fault. 

    More formally (taken from Liquid Haskel slack):  Just like
	
	    cAssert b
	
	requires b as a precondition,
	
            cAssume b
	
	“Ensures” b as a postcondition!
	In a strict language you can write
        
	    cAssume :: b:Bool -> {v:() | b}
	    cAssume b = if b then () else diverge()
	    
"

[janvrany]

I'd name the parameter simply as condition or - if you prefer - aBooleanOrBlock because want to allow both plain Booleans and blocks (at the very least, to make it compatible with #assert:

[janvrany]

browsed for #assume: and #assert: but couldn't find it. Am I hallucinating?

Sort of. We talked about it and that resulted in janvrany/Tinyrossa#30. I did not yet started working on it.

[shingarov]

that resulted in janvrany/Tinyrossa#30.

Ah, yes, that's it! it was exactly reading TR30 that I was trying to find.

[shingarov]

Wait, where did my explanation go???

[shingarov]

Did the exended comment on Bohr–Sommerfeld just disappear????

[janvrany]

Did the exended comment on Bohr–Sommerfeld just disappear????

Looks so, but I've got it.

I think the crux of the problem is elsewhere, namely in that right now we are writing something in-between Smalltalk-80 and Smalltalk-25.

Yes, that too. Let's leave this conversation for 2024.

I meant a much narrower scope for this PR: namely, just to save Prof. Jhala's wording somewhere before Slack eats it.

OK, fine with me then. Shall I merge it then?

[shingarov]

Yeah let's merge it for now.

Looks so, but I've got it.

In a notification email I guess?

[janvrany]

Yeah let's merge it for now.

Done.

In a notification email I guess?

Yes.

[shingarov]

Then maybe you can cut-and-paste that comment back here so it doesn't get lost?

[janvrany]

Then maybe you can cut-and-paste that comment back here so it doesn't get lost?

Sure, good idea:

I meant a much narrower scope for this PR: namely, just to save Prof. Jhala's wording somewhere before Slack eats it.
As to the "risk of unleashing a wider and opinionated discussion", I think the crux of the problem is elsewhere, namely in that right now we are writing something in-between Smalltalk-80 and Smalltalk-25, akin to Bohr–Sommerfeld vector model: already not Galileo–Newton's classical physics, but not yet quantum mechanics.
I have just now created #181 to address your concerns in proper Smalltalk-25.