|
Ron Pressler
@
pressron
London
|
|
Views are my own. Retweets are not endorsements.
|
|
|
5.806
Tweetovi
|
333
Pratim
|
1.157
Osobe koje vas prate
|
| Tweetovi |
| Ron Pressler proslijedio/la je tweet | ||
|
Damien Kempf
@DamienKempf
|
29. sij |
|
I always tweet about H. Bosch, but Pieter Brueghel the Elder is another (contemporary) genius. Let's take a look at his 'Dutch Proverbs'. pic.twitter.com/3JYJOsPpVw
|
||
|
||
|
|
Ron Pressler
@pressron
|
28. sij |
|
Not the same, as Haskell doesn't have the same notion of stack context. Composition is also better than monad transformers, although the feature does resemble algebraic effects minus the effect tracking, which we don't want (but could be added by languages that want it).
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
19. sij |
|
They even knew *how* the negative answer would be proven once the question was precise enough -- by diagonalization. But until Turing, no one could find a convincing and precise definition of computation.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
19. sij |
|
Everyone knew that the Entscheidungsproblem would be answered in the negative after Gödel's incompleteness. The problem wasn't getting the answer, but forming the question more precisely by defining what an algorithm or a calculation is.
|
||
|
|
||
| Ron Pressler proslijedio/la je tweet | ||
|
41 Strange
@41Strange
|
17. sij |
|
Sphynx Cat’s Paws pic.twitter.com/6HqpRFMLIa
|
||
|
|
||
| Ron Pressler proslijedio/la je tweet | ||
|
|
41 Strange
@41Strange
|
17. sij |
|
The Hammer-headed bat pic.twitter.com/KAye2CrKhC
|
||
|
|
||
| Ron Pressler proslijedio/la je tweet | ||
|
Medieval Death Bot
@DeathMedieval
|
17. sij |
|
Thomas de Baeton, died 1345, slain by a clerk long after curfew
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
15. sij |
|
lamport.azurewebsites.net/tla/hyperbook.…
TLAPS might not be efficient enough for regular industry use, but it's good for people publishing algorithms.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
15. sij |
|
You can also use TLA+'s proof assistant to write general proofs (even with infinite sets).
Fun fact, "model" in model checker comes from "model" in logic -- a satisfying assignment -- and not from "model" in the mock-up/representation sense used elsewhere in your tweet.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
13. sij |
|
I think that temporal quantification should allow you to express hyperproperties that could be expressed with no quantifier alternation on the behavior, but I'm not at all sure.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
13. sij |
|
Wouldn't ∃ t ∈ Int : *∀* vars : Spec ⇒ ◇□(x = t), where *∀* is temporal quantification, work in TLA+? /cc @lemmster
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
12. sij |
|
I think we should make understanding make delivery cheaper. After all, software is written to serve a real-world purpose, not our intellectual curiosity, and it's reasonable to focus on that goal, but we can try to make understanding a better means for achieving it.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
12. sij |
|
I personally agree, but I don't like saying that things that are easier for you or me are "objectively easier." Subjective is sometimes the best we have, and often it's good enough.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
12. sij |
|
TLA+, unlike some other specification languages with model checkers and/or proof assistants, is mathematics and not programming because that is what allows it to be so powerful and flexible. If you still prefer programming perhaps you'll find those other tools more to your taste.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
12. sij |
|
The missing piece is PlusCal. PlusCal, unlike TLA+, has programming language semantics. I hope that, in light of my notes, you'll understand why it must be distinct from TLA+, and that the distinction is helpful.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
12. sij |
|
I've written a couple of notes that explain why I think your objections are misplaced:
old.reddit.com/r/tlaplus/comm…
old.reddit.com/r/tlaplus/comm…
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
11. sij |
|
Note that none of the dogmas has been verified or even observed in any scientific way. We have no rigorous knowledge of what's productive and what's not, mostly aesthetic dogma about all the way down. Scientists debating Beatles vs. Rolling Stones (I like large subroutines :)).
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
10. sij |
|
You'll be able to declare inline records that will have the compact representation; that just has to wait for inline types.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
10. sij |
|
Right, but their definition ends up being exactly what you'd get if the superclass were a component rather than a superclass, and it does not behave as idiomatic objects normally should, i.e. a method (indirectly) uses reflection to change how it works with subtypes.
|
||
|
|
||
|
|
Ron Pressler
@pressron
|
10. sij |
|
They are separate features, but records would also make for good inline classes.
|
||
|
|
||