SubjectToChange

https://coq.discourse.group/t/coq-community-survey-2022-resu...

You have to write more code, and in a different language, but unlike just testing you can actually prove that invariants hold for all possible inputs.

Formal verification is needed to show that the code actually implements a specification. If anything, a formal specification is really good for generating test suites for the implementation code.

Just look at the suppliers working on the SLS SRBs and those working on the LGM-35 program, perhaps then you'll see the extent of the overlap. Furthermore, you might want to look into why the space shuttle had the architecture it did, and why space shuttle SRBs were being shipped out of Utah. Large scale SRB manufacturing has been, and continues to be, an enormous problem for the DoD. Hence why wasteful programs like SLS exist.

SLS was never about being the most practical and/or efficient launcher. It is a pork barrel project, but one with an important role. In particular, it is maintaining vital aerospace industrial capacity. If the US wants things like ICBMs then programs like SLS are a necessary evil.

There are specific scenarios that a major issue, yes. But as the title of the video implies, the problem with exceptions runs far deeper. Imagine being a C++ library author who wants to support as many users as possible, you simply couldn't use exceptions even if you wanted to, and even if most of your users are using exceptions. The end result is that projects that use exceptions have to deal with two different methods of error handling, i.e. they get the worst of both worlds (the binary footprint of exceptions, the overhead of constantly checking error codes, and the mental overhead of dealing with it all).

C++ exceptions are a genuinely useful language feature. But I wish the language and standard library wasn't designed around exceptions. C++ has managed to displace C almost everywhere except embedded and/or kernel programming, and exceptions are a big reason for that.

The C and C++ standards are quite minimal and whether or not an implementation is "compliant" or not is often a matter of opinion. And unlike other language standards (e.g. Java or Ada) there isn't even a basic conformance test suite for implementations to test against. Hence why Clang had to be explicitly designed for GCC compatibility, particularly for C++.

Merely having a "language standard" guarantees very little. For instance, automated theorem proving languages like Coq (Rocq now, I suppose)/Isabelle/Lean have no official language standard, but they far more defined and rigorous than C or C++ ever could be. A formal standard is a useful broker for proprietary implementations, but it has dubious value for a language centered around an open source implementation.

Fujitsu actually does sell their A64FX processors. In fact, they are running in one or two European super computers[1][2]. Still, that's not to say that buying them Fujitsu is easy and/or straightforward.

[1]: https://www.hpcwire.com/off-the-wire/fujitsu-selected-to-del...

[2]: https://www.youtube.com/watch?v=yInhWFztvXs

Probably for the same reason Intel/AMD doesn't get rid of the rest of the cruft in x86-64, i.e. backwards compatibility. Additionally, there would be issues with Intel/AMD leveraging an optional weak memory model in their chips without compromising the performance of legacy TSO applications. They are probably better off making x86-64 perform best under TSO.

Apple Silicon supports both Arm's relaxed memory model and Intel's TSO for backwards compatibility. Microsoft is doing the same for Windows on Arm.

I’m not going to pay thousands for a commercial license

In the vast majority (90% or more) of cases the performance between Matlab and Mathematica is identical or within the margin of error. And where performance does differ substantially, Matlab isn't always coming out on top. So the question then becomes whether or not your work depends on those particular use cases. In my eyes, the Wolfram Language is fundamentally superior to Matlab. And even if Mathematica/WL lags behind Matlab is some numerical aspects, Wolfram Research will have a far easier time fix or improving that deficiency than MathWorks will have improving the poverty of symbolic computation in Matlab.

Of course, the factors in practical use cases are quite a bit more complex than what I've said above. If you're working at an engineering firm that's already knee-deep in Simulink and various Matlab Toolboxes, then the choice has been already been made for you. And sometimes it's not a question of performance but one of feature parity, e.g. Compile in the Wolfram Language vs Matlab Compiler/Runtime. Also, the complexity of the Wolfram Language is not a benefit for users looking to simply write code and get a result ASAP.

Personally I am quite fond of Mathematica (well, the "Wolfram Language") and I'm happy to pay for the hobby license price. Not only do I think I'm getting my money's worth, but I think supporting mathematical software is a "good cause" to put money behind. Moreover, I've never understood why people like amateur photographers will often spend more on tools like Adobe CC than many programmers (amateur or otherwise) spend on their tools period. Or why someone would spend $20-40+/month on various subscription services only to balk at $200-$400 licensing fees. Then again, I spend more time in Mathematica than I do in almost any other program installed on my computer.

However there is still an important place for (F)OSS mathematical software. As comprehensive as Mathematica usually is, it still has some significant shortcomings in advanced mathematics. In particular, I have a hard time believing it will ever fulfill those more "niche" areas of mathematics for two reasons. First and foremost, the ROI drops off a cliff for more advanced and/or esoteric fields. Second of all, the Wolfram Language already has 6000+ built in functions, so adding hundreds more to comprehensively support of something like Group Theory just doesn't make sense. Sure, they could be supported via packages, but that comes at the cost of performance (no first class support in the kernel) and usability (users have to go out of their way to use it).

Therefore, (F)OSS software like GAP, M2, and PARI/GP serve an important role in "rounding out" the gaps in the wolfram language. In my case, I contribute to FOSS projects an equal amount to whatever I spend on my Mathematica license. Or when monetary contributions to a project are not so straight forward, I try and contribute my time and skills improving them.

To be frank, I don't care much for projects trying to replicate Mathematica's functionality. Of course people are still going to develop and improve them, which at the very least puts some pressure on Wolfram Research to constantly improve basic functionality, but it will probably take one or two decades for said projects to replicate what Mathematica/WL is today.

[1]: https://www.wolfram.com/raspberry-pi/ [2]: https://www.wolfram.com/mathematica/pricing/home-hobby/

Database defaults in general are a touchy topic. Whatever set of defaults are chosen will be suboptimal for almost any serious user. A far more serious issue is figuring out the actual behavior of a database in different configurations. For instance, Oracle's SERIALIZABLE transaction isolation level only offers snapshoot isolation.

Simply making C++ compilers compatible with one another is a constant struggle. Making Rust work well with existing C++ code is even more difficult. Thus, it is far easier to make something like Clang understand and compile C++-specific annotations alongside legacy C++ code than making rustc understand C++ types. Moreover, teams of C++ programmers will have an easier time writing annotated C++ than they would learning an entirely new language. And it's important to recognize how deeply entrenched C++ is in many areas, especially when you consider things like OpenMP, OpenACC, CUDA, HIP/ROCm, Kokkos, etc etc etc.

WG21 hasn't been able to solve the restrict type qualifier, or make a better alternative, in over twenty years. IMO, hoping that WG21 adequately solves Safe C++ is nothing more than wishful thinking, to put it charitably.

>(a) You do not know how or where Facebook use BTRFS

Their engineering team has posted a few of their use cases.

>(c) Facebook probably employ the guy who invented BTRFS and an army of kernel developers on top of that .... how much in-house support do you have for BTRFS ?

Uh, about as much as any other file system? Those changes and improvements are upstreamed to the kernel anyway. It's not like Facebook has some sort of special version of btrfs they are using.

>As far as I am concerned, the fact that they STILL have not fixed RAID5 in BTRFS says everythng you need to know.

As far as I know, the issue with RAID5 in btrfs is highly complex and it would take quite a bit of dedicated effort to make it work. I suppose it's a architectural shortcoming of btrfs. But then again, it's RAID5, a/k/a something only shoestring hobbyists really care about. Hence why no one is bothering to make it work in btrfs.

At the end of the day, btrfs is perfectly fine for home users and workstations. ZFS beats it out on servers, that's fine. Traditional filesystems are not the end-all be-all of storage anymore. No one has made a better ZFS because the industry has moved on to things Ceph, vSAN, AzureHCI, etc.

Incrementally replacing C code with Rust is far, far easier than C++. For instance, passing null-terminated strings to Rust code is quite straightforward, whereas a std::string absolutely is not.

C will live for a very long time, but C++ will live even longer. Maybe that sounds absurd, but the fact is that every major C compiler is written in C++, and the rest of the toolchain is moving that direction if it isn't already there.

Not quite. I doubt librsvg would have been ported to C++ if Rust didn't exist. Nor do I believe that C++ would have been allowed into the Linux kernel as readily as Rust currently is, e.g. Android's binder.

Sure, Rust is a small language, but it is making consistent progress and it is only becoming more of a viable C replacement. Of course, C isn't going anywhere and the vast majority of C code is not going to be rewritten in Rust. However, that is normal in the lifecycle of programming languages, i.e. codebases are not usually rewritten, they simply become obsolete and are replaced. Just like Java didn't need to replace every line COBOL to become the enterprise language of choice, Rust doesn't need to replace C everywhere to become the preferred systems programming language.

That basically implies name mangling in some form or another, i.e. good luck trying to convince C programmers of such a thing.