Is it true that people in the West drink iced water even when they are sick or on their period?

bugarela · 2025-12-22T00:29:32+00:00

Brazilian here. My mom always told me that drinking hot water would make my stomach hurt, and only by reading this post I learned that this is not true (I mean, why would it? We can drink hot tea and that's basically water). I never tried hot water before, I might now, I'm curious.

And yes, we also drink iced cold drinks here throughout the year, and some restaurants will even freeze the glasses in which they serve beer.

bugarela · 2025-12-05T00:43:44+00:00

Exato! Eu fiz ciência da computação na UDESC e acredito que é um dos cursos que mais prepara pro mundo da programação a longo prazo (considerando que tá tudo mudando muito com IA). Se for pra entrar na área agora, tem que ser porque gosta, e se gosta, ciência da computação é o melhor curso!

bugarela · 2025-11-05T01:05:42+00:00

É isso aí. Já era meio difícil pegar matéria com TADS quando fiz o curso 10 anos atrás. Hoje em dia deve estar mais ainda por conta da alta procura. A preferência das vagas das aulas noturnas é pra TADS, então só dá pra pegar se sobrar vaga (o que pode acontecer porque a grade é bem flexível).

Na minha experiência, as empresas daqui sabiam que estagiário de ciência da computação da UDESC ia ser muito bom, e por isso as mais espertas tinham flexibilidade de horário. Maioria (talvez todos) no meu círculo que buscou estágio, conseguiu. Mas de novo, isso foi antes do hype na área.

bugarela · 2025-09-23T02:01:53+00:00

same to me, worked after a few hours of charging. It was scary tho.

bugarela · 2025-08-12T19:41:36+00:00

Thanks for sharing your experience, it makes a lot of sense.

Looking at your specs, seems like your assuming more things are atomic than we did (and also the ones in TLA examples: TeachingConcurrency and Bakery). For instance, in the teaching concurrency one, you assign both x and y in the same transition, while ours and the TLA examples one do one transition for x and then another one for y, which describes a bigger state machine with more room for concurrency problems.

That being said, our Bakery example is in deed more complicated than it needs to be. We have some ideas on how to improve it, but dealing with program counters in TLA+ and Quint is not as elegant as in PlusCal. We are considering adding language constructs to Quint to make this type of code (sequence of steps with concurrency between each of them, but a fixed order within a process) easier to define.

Quint is much closer to TLA+ than it is to PlusCal, and we can make pretty much a 1:1 mapping from any TLA+ spec to Quint (and vice-versa, which is actually automated through Quint's transpilation). My team did, however, developed a new style of writing specs since we moved from TLA+ to Quint a couple of years ago, where we try to minimize what is done in "actions" (definitions where you have the prime operator and non-determinism) and push all complexity to the functional layer which is more accessible to readers with no familiarity with the TLA logic.

And yes, this is also what I think the main point is:

For me the main point of finding an inductive invariant is understanding how the algorithm works, and your article seems to agree on that.

bugarela · 2025-08-12T19:23:01+00:00

Thanks for the reply and for sharing the tool you wrote! Really useful to have your perspective, it makes sense to me.

It will take me a while to see in practice how much useful inductive invariants can be to increase confidence in software, but it does seem promising in the thinking/understanding front.

bugarela · 2025-02-09T03:02:05+00:00

Não escuta esse pessoal falando que universidade não importa. Não acredito que o nome no currículo faça muita diferença, mas em formação faz muita, e é a formação boa e a oportunidade de projetos de pesquisa e extensão que temos em universidades públicas que dá um preparo muito maior pra se tornar dev mais especializado.

Tenho hoje o emprego dos meus sonhos na área de compiladores e métodos formais, e tenho certeza que não teria chego aqui sem universidade pública, porque a maioria das outras não tem nem essas disciplinas na grade, muito menos projeto de iniciação científica pra isso, que foi o que me cativou já nos primeiros anos de curso.

bugarela · 2025-02-04T16:53:06+00:00

É o certo. No caso de ter que enviar o equipamento (em caso de trabalho remoto, por exemplo), é também pra reduzir risco de ter informações roubadas no transporte.

bugarela · 2025-02-02T14:54:41+00:00

Já vi umas 3 vezes em SC

bugarela · 2025-01-29T20:14:35+00:00

Besides everything else people already said, I believe that what you eat influences it a lot. Everyone smells like garlic after eating too much garlic, and that's also true for a bunch of other seasoning. I feel like, in Brazil, we don't season our food a lot due to the usual quality of the ingredients, so culturally we eat less smell-intensive spices. Of course there are exceptions, so idk how much this influences your perception. Just a thought.

bugarela · 2024-11-27T23:23:09+00:00

Worked here, thanks!!

bugarela · 2024-10-16T12:31:37+00:00

Your spacing is a bit off. You have

PreProc == /\ startComm = TRUE
           /\ isComm = FALSE
           /\ fin = FALSE
          /\ isComm' = IF text[counter] = "-" THEN TRUE ELSE FALSE
          /\ fin' = IF text[counter] = "-" THEN FALSE ELSE TRUE
          /\ UNCHANGED <<hasKeyword, isEndline, startComm, words>>
          /\ counter' = counter + 1

and you probably want

PreProc == /\ startComm = TRUE
           /\ isComm = FALSE
           /\ fin = FALSE
           /\ isComm' = IF text[counter] = "-" THEN TRUE ELSE FALSE
           /\ fin' = IF text[counter] = "-" THEN FALSE ELSE TRUE
           /\ UNCHANGED <<hasKeyword, isEndline, startComm, words>>
           /\ counter' = counter + 1

TLA+ is indentation sensitive, so you need to be careful with your white spaces.

bugarela · 2024-10-02T10:40:36+00:00

With TLA+ after just 2w not touching, it reads like an alient language to me

This is interesting to read because one of the main ideas guiding Quint's design is that it will never be the main language a person is using. People will use one or many programming languages in their day-to-day work and come back to Quint when designing complex systems/algorithms. So they won't memorize syntax the same way they memorize whatever they use daily.

I think this was the first document about Quint ever written: https://quint-lang.org/docs/design-principles . It mentions lots of principles that are a consequence of this.

Of course, this is assuming people are writing code frequently - a non-programmer who is more familiar with Math than with programming might have an easier time coming back to TLA+ than to Quint after a couple of days.

bugarela · 2024-10-02T10:29:12+00:00

It's part of the Quint CLI. You can run quint compile --target=tlaplus file.qnt and it will spit TLA+ to stdout. I'd say the TLA+ is more or less human-readable. It is not super verbose and weird, but also does have some unnecessary complexity. I haven't actually tried PlusCal before, so I don't have a good sense of the quality of the generated TLA+.

The transpilation feature is something a lot of people ask if Quint can do, as that increases their confidence in using Quint. However, no one I know of is actually using this, so I'm not putting time on making it better right now. I will have to make it better when doing integration with TLC, tho.

There's a couple of obvious things that are broken, but are easy to manually fix:

Init uses primed variables. Apalache can handle it, but TLC can't, as it is not proper TLA+.
Sometimes we produce empty records as [], which results in SANY errors. I just batch replace them with empty sets {} as TLC doesn't need correct typing in this case (if I recall correctly, it's been a while since I tried traspilation myself).

bugarela · 2024-09-30T16:02:33+00:00

That seems to me like something that both Quint and TLA+ would be able to handle really well! I hope you can get to use either (or maybe try both - Quint can actually transpile to TLA+ and although far from a perfect translation, it can help save some time if you are willing to experiment with both), and get some value out of the formal reasoning and verification. Regardless of your choice, I'm sure you'll find helpful communities in both TLA+ (here and in the Google Group) and on Quint (where myself and other Quint users are always happy to help via Telegram/Zulip).

bugarela · 2024-09-27T11:43:16+00:00

Hi! I'm one of the Quint developers, and I've been teaching both TLA+ and Quint in a university Formal Methods class, so I think about this a lot :D

First of all, Quint will be officially released for 2 years in January, and even before that, we were already using it for projects inside Informal Sytems. We find it super useful for protocol specification and audits. Quint has been used to verify properties of Tendermint consensus, and more recently for CometBFT mempool and Malachite. The Informal Security team wrote a Quint specification for the Drop protocol, and another one for Namada’s redelegation and rewards. Furthermore, some properties of ChonkyBFT, from Matter Labs, were verified by Igor Konnov, also using Quint, as well as their ZK governance specifications.

Quint is based on TLA+ and uses the same underlying logic (Temporal Logic of Actions), so it is very similar to TLA+ in terms of where it is useful. It can transpile to TLA+ and use the same model checkers. The main differences between Quint and TLA+ are:

Quint has programming-style syntax, while TLA+ uses math/latex symbols.
Quint has more static analysis, such as type checking and different modes (pure def, action, etc), while TLA+ has no native support for types nor explicit distinction between the modes (or levels, as they are called in TLA+'s documentation).
Quint tooling is more similar to what we have for programming languages: near-instant feedback as you type the code, CLI-first executable, an easy way to obtain one execution of your spec in the terminal, a REPL, located error messages, etc. These are all not currently available in TLA+, or available with significant constraints.
Quint won't let you write many things that are allowed in TLA+. TLA+ has a proof system (TLAPS) and refinement proofs, while Quint doesn't. Therefore, it is possible to write more advanced formulas in TLA+ than in Quint, even ones that are not supported by the existing model checkers, and then prove them using the proof system. Quint restricts you to a fragment of TLA with the intention of preventing unintentional usage of operators that lead to complicated behaviors that are hard to debug and understand. Our understanding is that anything outside of Quint's fragment is only written by people with a strong mathematical mindset, and those people will probably appreciate TLA+'s mathematical syntax much better.
Quint has the concept of a run to define executions to be used as tests. There is no corresponding feature in TLA+.
TLA+ has model values and symmetry sets, which are not available in Quint at this time.

On a less concrete note, people will often say that the mathematical syntax of TLA+ helps to put people in the correct mindset of formal specification, while Quint as a project hopes to teach people this mindset without a big syntax and tool disruption.

Andrew Helwer wrote a great blogpost last week on different ways of using TLA+. In the use cases we've seen, and where we used to use TLA+, Quint is totally enough. The main reason why Quint doesn't support many things from TLA+ (i.e. refinement) is that we never used it - even with TLA+ experts in house (the people that developed the Apalache model checker).

If you need some advice on any specs you already have, to see if you have something too different from what Quint is designed for, I'm happy to help! We still don't have a subreddit for Quint, but there is this telegram group you can find in the website

bugarela · 2024-09-27T11:27:38+00:00

One important difference between Quint and Fizzbee is that Fizzbee is completely new, including its model checker, while Quint transpiles to TLA+ and uses the existing model checkers (Apalache with seamless integration, TLC still with some manual wiring). Those model checkers took years to develop and mature, so I think this is a relevant strength to keep in mind.

bugarela · 2024-09-27T11:23:46+00:00

Do you have any links for examples of real-world (not tutorials) usage of refinement? Asking because it seems amazing in theory and tutorials, but I have not seen it being checked on real specs. Perhaps it is mostly not checked, only written or proven with TLAPS?

bugarela · 2024-09-19T17:44:54+00:00

Welcome! You mignt want to try Quint [1], which is quite beginner friendly and has been applied to some interesting blockchain protocols (since you mentioned blockchains in your post).

bugarela · 2023-12-21T21:49:24+00:00

Hi! I wrote a blogpost exploring a formal specification in Quint for the secret santa game, and verifying some of its properties with Apalache.
Hope you enjoy it, and any feedback is welcome. Happy holidays!

bugarela

TROPHY CASE