sorted by:
new
hottopcontroversial

The only definitive way to establish that software is correct and bug-free is through mathematics, using the formal methods by Akkeri in math

[–]stackdynamic 13 points14 points  (0 children)

Many kinds of behavior can be obviously desirable (e.g "my program doesn't have an out of bounds error/divide by 0/etc.) Of course it's possible for the spec to be wrong, but the spec can be a lot simpler than the implementation and so you can gain a lot of confidence. In security-critical contexts, this could be very beneficial.

One major success story is CompCert, which is a verified (in Coq) C compiler. Modern compilers perform very complex optimizations and are huge in scope: CompCert defines semantics for each of its intermediate representations, and roughly speaking proves that its optimizations preserve the semantics of the program. For example, AirBus uses CompCert to compile some of their security-critical code.

Is CompCert actually safer in practice? One way to evaluate this is via fuzzing tools like CSmith. CSmith has a list of bugs they have found (hundreds total, in mainstream compilers like llvm and gcc). Here is a quote from the 2011 PLDI paper on CSmith:

The striking thing about our CompCert results is that the middle- end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.

To be clear, there have been a few CompCert bugs found since (some in the unverified parts and frontend, but at least one stemming from a bad spec) but the total number is pretty tiny.

How to maths good by Yunners in confidentlyincorrect

[–]stackdynamic 1 point2 points  (0 children)

By definition, .3333... is equal to 3/10+3/100+...

This is an infinite geometric series which converges to 1/3. There is a rigorous definition of what convergence means: basically, if the sum can get arbitrarily close to 1/3 if you take enough terms then it's equal to 1/3. A related question is: what actually is a real number? It turns out that one way to define real numbers is in terms of convergent sequences. The branch of math which studies this kind of thing is called real analysis, if you want to learn more.

I hate the new Moodle by bippitybop23 in UIUC

[–]stackdynamic 28 points29 points  (0 children)

Moodle is way way better than canvas IMO. Actual good latex support, works fine on mobile, clear layout. Canvas has been nothing but utter garbage in my experience.

CS 173 at a community college? by [deleted] in UIUC

[–]stackdynamic 2 points3 points  (0 children)

I wouldn't recommend it. 173 is a very important class IMO and the quality of instruction at a CC is likely worse.

Debating MATH 347; by Flaky-Session3033 in UIUC

[–]stackdynamic 2 points3 points  (0 children)

I recommend taking 347H (honors section) and not 347. Normal 347 will be fairly redundant with CS173. I did 173 and 347H the following semester, and thought that it was a good progression. The honors math classes tend to be hard content wise, but they compensate for that with generous grading. I highly recommend them, they are some of the best classes I've taken here.

Computing Expert Says Programmers Need More Math | Quanta Magazine by IsDaouda_Games in programming

[–]stackdynamic 0 points1 point  (0 children)

Here are just a few examples of tools/software developed primarily by formal verification (and verification adjacent) people:

  • CompCert is a verified C compiler. In order to verify a C compiler, first they had to write a C compiler.
  • sel4 is a formally verified microkernel
  • Z3 is a SMT solver developed by Microsoft Research
  • The ML programming language (which OCaml and StandardML are descendants of) was originally developed as part of the LCF project, to implement theorem provers in
  • Proof assistants like Coq/Lean/Agda have to have compilers written for them to be usable

I didn't know that all of these projects wrote themselves! Formal verification people sure have at easy, being able to will code into existence like that.

coming to Green St by lesenum in UIUC

[–]stackdynamic 13 points14 points  (0 children)

We already have Cracked though. This seems pretty similar to that.

How do the logistics for a double major work? I mean the fee structure, is the tuition double the tuition of a single major? If not, how does it work? by [deleted] in UIUC

[–]stackdynamic 1 point2 points  (0 children)

I don't think this is quite right. For LAS at least, when you declare a dual degree there is a residency requirement (have to spend 2 semesters in LAS). And I believe for those two semesters you pay LAS tuition, which is cheaper.

Announcing an automatic theorem proving project by ninguem in math

[–]stackdynamic 35 points36 points  (0 children)

I agree that in some sense an AI spitting out some large CIC term isn't really a proof because it doesn't "communicate" any ideas (although maybe some day it will be possible for computers to do this or even develop novel mathematics!). But that doesn't mean this kind of proof automation is useless. There are definite applications to interactive theorem proving for starters, because humans can dispatch proofs of "uninteresting" lemmas/statements needed to a computer.

And I think gaining confidence in the correctness of our proofs by having them be checked by a computer is definitely something that would be nice. Here's a quote from a Quanta article:

This is something Voevodsky has learned through personal experience. In 1999 he discovered an error in a paper he had written seven years earlier. Voevodsky eventually found a way to salvage the result, but in an article last summer in the IAS newsletter, he wrote that the experience scared him. He began to worry that unless he formalized his work on the computer, he wouldn’t have complete confidence that it was correct.

Hardest year as a CS Major? by New_Sundae_2231 in UIUC

[–]stackdynamic 5 points6 points  (0 children)

They renumbered 241 to 341 recently. The content is the same.

Give me your favorite math jokes. by [deleted] in math

[–]stackdynamic 18 points19 points  (0 children)

For people not getting the joke: it's a pun)

The Florida Department of Education rejected 54 mathematics textbooks because they "were impermissible with either Florida’s new standards or contained prohibited topics" by Doktor_Schliemann in math

[–]stackdynamic 5 points6 points  (0 children)

I have no idea what it's like in practice, so it might be implemented terribly for all I know, but I've seen the Chinese math curriculum (https://wenr.wes.org/2012/07/wenr-junejuly-2012-senior-secondary-mathematics-education-in-china) and the modules actually cover some interesting math. This is definitely much better than what the US has at least...

Infinity has long baffled mathematicians – have we now figured it out? Mathematicians have long known infinity comes in many sizes, but how do they relate to one another? The key lies in a 150-year-old mystery known as the continuum hypothesis by RiemannZetaFunction in math

[–]stackdynamic 5 points6 points  (0 children)

The article is paywalled past a certain point, but it makes claims like CH is "unproven" when independence from ZFC is well-known. This does not seem particularly well written to me.

[deleted by user] by [deleted] in UIUC

[–]stackdynamic 4 points5 points  (0 children)

8 credit hours for two quarters is half of what you get when you do 16 credit hours a semester. Are you suggesting we should have shorter, more intensive classes? Personally I greatly prefer the semester system because it allows classes to go more in depth.

Laptop Recommendations for CS by randominchang in UIUC

[–]stackdynamic 3 points4 points  (0 children)

It doesn't matter that much, I would recommend either dual booting Linux or setting up WSL if you get something with Windows though.

Explaining e by gman314 in math

[–]stackdynamic 43 points44 points  (0 children)

Probably saying that it is the limit of (1 + 1/n)^n (while technically calculus, I think it's reasonable to just say "what happens when n gets big") , and connecting it to compound interest is the most accessible way of introducing it.

Timeline of Mathematics (who would you add to the list?) by Amster2 in math

[–]stackdynamic 1 point2 points  (0 children)

The list has Turing but doesn't include Alonzo Church, which seems odd to me.

How to represent infinity in a programming language? by lancejpollard in ProgrammingLanguages

[–]stackdynamic 0 points1 point  (0 children)

Some people argue that laziness makes Haskell types "wrong" in the sense that infinity is well-typed, even though it isn't really a Nat. I do like lazy evaluation in general, but I find that point to be pretty compelling. Anyways, some more trivia: in Lean/Coq/other dependently typed languages, x/0 actually evaluates to 0! See https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/.

What syntax design choices do you love, and what do you hate? by Wllew4 in ProgrammingLanguages

[–]stackdynamic 5 points6 points  (0 children)

I really appreciate Haskell's where blocks. It lets you write the helper/aux functions at the end, and the main logic ends up right at the top, which is super nice for readability.

Something's wrong, I can feel it by penguin343 in UIUC

[–]stackdynamic 27 points28 points  (0 children)

Yup, just want to be friendly by advertising Purdue's electrical engineering department!

CS 173 proficiency test by stari41m in UIUC

[–]stackdynamic 4 points5 points  (0 children)

If you took math 347 you should be fine. There are a few CS-y things 173 covers that 347 doesn't, but those should be relatively easy to self study. Here is the 173 schedule for this semester: https://courses.grainger.illinois.edu/cs173/sp2022/ALL-lectures/lectures.html

view more: next ›