scscsc

Do you also think that primary school students should not be taught, say, multiplication? Because they can, of course, use a calculator. No need to ask them what 3 times 4 is.

For your convenience, here is the list of NP-complete problems where "AI" works better than the state of the art in the worst case:.

Having some experience in this field, I can say that all of the tools presented on the webpage are very lightweight static analyzers. They are all based on processing the syntax tree and they which will detect things like uninitialized variables, or do style checks.

"Real" static analyzers, which are more useful, are based on symbolic execution and abstract interpretation and they will uncover more interesting classes of errors, like double frees, out of bounds array access, etc.

Note that all analyzers will have FPs and FNs, because the underlying problem is uncomputable.

The best open source "real" static analyzer overall for C++ is the Clang static analyzer. There are many commercial analyzers available, and most C++ shops will use one or more of these.

Does anyone know anything about the affiliation of the first author, "Fgemm SPA"?

It does not stop it, but certainly reduces it.

What are the dozen ways?

I have just seen someone using such a phone.

It looks good, just a tiny bit bulky.

Not sure on how it will do long term.

My OnePlus has been serving me well for more than 3 years now.

Note that the title is misleading.

The issue is lack of seatbelt pre-tensioning, not the size of car.

I am surprised manufacturers are not required to have pretensioners.

To those wondering if there will be a successful "marriage" between popular incarnations of AI, like ChatGPT, and FM: no, at least not in the sense you would expect.

Sure, ChatGPT will successfully manage to find formal proofs that have been done before.

But synthesising proofs from scratch is NP-complete for the simplest proofs (or worse for more interesting cases), and LLMs are simply not clever enough to do it (except in cases where the proof has been seen before).

It could be possible to integrate an SMT solver with a LLM to make this work, but the core difficulty of the FM task will then be solved by the SMT solver.

I would like to point out that such a resource is useful for reference purposes (only).

If you want to really understand an algorithm/a data structure, you have got to read it up and get your hands dirty and implement it yourself. There is no way around this.

This is a bit like taking notes in classes. The notes themselves are (nowadays mostly) almost worthless, with easy access to textbooks and other resources. The fact of taking the notes is what actually counts.

Could anyone in the know explain how "shorting" works?

I am surprised so many talented engineers went the touchscreen route. Volkswagen, Mercedes and more recently BMW are going this way. In my experience it is not only annoying, it is a safety hazard. In my old car, I could feel for the button to turn on the defrosting without ever taking my eyes off the road, it was so well designed!

In a way, it feels that the current trend is very much like the Apple laptops at some point, where they god rid of the physical function keys and replaced them with touch sensitive controls. Thankfully, Apple is reverting this change.

I think at some point car manufacturers will realise that it leads to more accidents and they will also reverse course. Perhaps touchscreens will even be forbidden?

Caveat: I was wrong before on touchscreens. I though phones with touchscreens will not work out, but they have. However, it is because we no longer use phones for phoning, but to watch movies, read text, etc.

I have an anecdote to offer: in the early 2000s I was learning to drive in a former comunist country. Most cars were Dacia 1310, a copy of 1970s Renaults. The stick was awful, the steering was very heavy (as in lifting weights heavy), the clutch was terrible. It was very difficult to drive one, let alone learn to drive one. Newer and better cars were just beginning to appear, but there were few of these and they were expensive. There were two lines of thought in my circle: (1) that you should learn on a Dacia, because then you will be able to drive anything and (2) you should learn on a modern car, because it is easier. Needless to say, camp (2) won: the Dacias all but disappeared and furthermore, newer cars are mostly automatic.

So I wouldn't hold my breath that the manual gear shift will survive.

When a field is young, it is simpler to make important discoveries, so in that sense, science is (obviously) getting harder.

But most of the graphs can be explained by the sheer number of papers being published.

Academics have the perverse incentive to publish as many papers as possible, instead of discovering as many interesting things as possible, because items published is way easier to measure than real progress made.

Therefore there is a significant paper inflation problem. People might today write 10 papers with LPUs (least publishable unit) with stuff that would have been a single technical report 30 years back.

This is much worse than it sounds, because it affects productivity significantly in subtle ways: it takes effort to publish those 10 papers, it takes effort to read up and review the 10x papers of others, and it takes time to think about LPUs instead of concentrating on the bigger picture.

Unfortunately, due to the way the research system is set up, it is not likely things will improve.

I am skeptical that a book can substitute for a mentor (or teacher) at the start of someone's dive into mathematics.

Once you know your basics, sure, go study a book. But by this point, you already know whether a given book helps you or not...

The internet has become larger.

People's attention is more dispersed (additionally, several platforms are actively fighting for their attention by using all tricks in the book).

Hence the signal-to-noise ratio has dropped. The people who would leave thoughtful comments are busy with other things.

A few communities still stand (hacker news included).

While losing weight, I would not replace it, but simply remove it altogether. Bread is not an essential nutrient (although obviously French baguettes are great tasting). You can get plenty of carbs from other food (e.g., fresh fruit).

You are probably thinking of F#, not F*. Very different languages.

The key here is "it looks like they are equivalent".

In fact, I am not sure they are equivalent (in general, without taking into account the context), and even if they were, proving this would be S.F. for a compiler today (2020). Even coming up with such an optimisation without hardcoding it does not seem plausible.

You are probably right regarding speed, but the article is definitely not pointless and bad.

That looks interesting. The code is not simpler to understand nor is it more efficient, but it seems to work, assuming target is in the list. How would you represent the empty list?

Not sure why you are being downvoted.

To have a truly fair evaluation, you would also need to know all the cases where science has not self-corrected yet.

It may not seem obvious to everyone, but the value is taking the notes (helps learning significantly), not reading them without context after the fact.

People who are interested in learning a subject without attending lectures would be better served by a textbook in the field.

I teach classes of ~500 students and classes of ~100 students.

While having individual projects is very nice and it works for smaller classes, it does not scale to average students.

I have once used individual projects to grade the ~100-student class and the amount of effort it takes is unbelievable.

For example, just your number "1." point, write a project proposal, is not so easy. It takes hours to write a good proposal and several back-and-forths between instructor and student to agree on a reasonable (not too advanced/not too basic) project.

Some might enjoy a teaser video of related work by some of the same authors: https://www.youtube.com/watch?v=baKHSXeIIaI. For context, the teaser was produced due to the conference going virtual because of the pandemic.

7. Another AI winter, despite AI/ML progress.

1. Mainstream CPUs get a lot more cores, making difference between software and hardware rendering disappear.

2. More and more features of programming languages for verifiable software (e.g., Dafny or Coq) get into mainstream languages, resulting in better overall software quality.

3. Computer mathematics (e.g., in Lean) gets traction, with some high-profile mathematics breakthroughs enabled.

4. Package manager-based attacks become more common.

5. Despite higher performance computers, a new level of abstraction in the process-container-vm stack makes up for performance.

6. Similarly, mainstream OSs will still lag and take seconds to, e.g., display the contents of the C drive.

As a teacher, the way to fix this is to give "aligned tests". That is, where the test tests for exactly what you want the student to learn. See https://en.m.wikipedia.org/wiki/Constructive_alignment.

As expressions, sure, they are not the same. But "2 + 3 = 5" is a statement about numbers, not about expressions. When you talk about numbers (the object of study), you do not (usually) talk about arithmetic expressions. Arithmetic expressions are part of the language used to talk about numbers.

When talking about arithmetic expressions themselves, you would use a meta-language (e.g., English). The arithmetic expressions would then be called the object-language (the language being studied). All of this should be pretty clear after taking a serious course in Logic.

I am not saying the choice of words is not sensible, I'm saying it it factually wrong.

The author unfortunately has a misunderstanding of equality.

Quoting him, "The equal sign is another mathematical concept that’s often misunderstood. It means, of course, that whatever is on either side of the equal sign is equivalent." This is actually wrong.

The equals sign (=) is a shorthand for stating not that the two sides are equivalent, but that they are the same (i.e., they are equal).

If they were just equivalent, we would use another sign, like ≡ (unicode U+2261).

I've worked on a similar project (https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html), where the interface allows only for backwards proofs. The only action allowed is to click a proof rule to be applied next, and the proof is presented in Fitch-like notation. Currently limited to propositional logic (not first-order).