In life-critical #engineering practice, #correctness and #reliability concerns always take precedence over cost, performance, and other factors.
In modern business #software practice, #cost considerations and #LLM hallucinations reign supreme. No other factors seem worthy of a consideration.
#Programming in a #dependent #type system does not imply a blind obedience to the type system by the #programmer: not all types need be adorned with fully-dependent regalia. That is, the programmer selects the desired level of type specificity. For example, we may type the all-too-familiar \(\texttt{qsort}\) with progressively finer specificity, as follows:
• Simple, parameterised typed:
\[
𝑞𝑠𝑜𝑟𝑡\ :\ [ℤ]→[ℤ]
\]
• Dependent, parameterised, indexed typed:
\[
qsort\ :\ (n : ℕ) ⇒ [ℤ\ n] → [ℤ\ n]
\]
• Fully-dependent, parameterised, indexed, predicated \(\Sigma\) type:
\[
𝑞𝑠𝑜𝑟𝑡\ :\ (𝑛:ℕ)⇒[ℤ\ 𝑛]→(𝑥𝑥:[ℤ\ 𝑛], 𝑆𝑜𝑟𝑡𝑒𝑑\ 𝑥𝑥)
\]
The closer we approach full dependence, the greater our burden of proof and the messier our #code. And the farther we retreat from full dependence, the less precise our type specifications and the weaker their #correctness guarantees.
Such is the thug-life of a programmer....🤷♂️
@hamishcampbell (4/9)
While I am #guessing that it must have been something along the lines of, if they can't see #past the first #impressions then I don't want them anyways. My opinion based on some #experience is that it also might have put off some right #people . And for something like this every single one #matters . Irrelevant whether that trait is #positive or #negative in them. I am not assuming my #correctness here.
...
A quotation from Judith Martin
It is, indeed, a trial to maintain the virtue of humility when one can’t help being right.
Judith Martin (b. 1938) American author, journalist, etiquette expert [a.k.a. Miss Manners]
“Miss Manners,” syndicated column (1999-02-02)
More info about this quote: wist.info/martin-judith/79642/
#quote #quotes #quotation #qotd #judithmartin #missmanners #correctness #ego #falsemodesty #humility #modesty #pride #rectitude #selfrighteousness
Use theorem provers to ensure the correctness of your LLM's reasoning
https://github.com/DebarghaG/proofofthought
#HackerNews #theoremprovers #LLM #correctness #reasoning #AIresearch #proofsofthought
I found https://rfd.shared.oxide.computer/rfd/400 today and really liked it! The examples of #async cancel safety are probably the most clear examples I've seen so far 😄
Thanks @rain for putting this together! #rust #correctness
Nice – more code-samples would’ve made it better:
“To Be a Better Programmer, Write Little Proofs In Your Head”, Nerve (https://the-nerve-blog.ghost.io/to-be-a-better-programmer-write-little-proofs-in-your-head/).
Via HN: https://news.ycombinator.com/item?id=44573409
See Also: “The Science Of Programming”, by David Gries.
Pedantry prides herself on being wrong by rules; while common sense is contented to be right without them.
Charles Caleb "C. C." Colton (1780-1832) English cleric, writer, aphorist
Lacon: Or, Many Things in Few Words, Vol. 1, § 48 (1820)
Sourcing, notes: wist.info/colton-charles-caleb…
#quote #quotes #quotation #qotd #cccolton #bureaucracy #commonsense #correctness #error #legalism #pedantry #procedure #rules
🚀 Welcome to the parallel universe where #AWS apparently cares about 'correctness' instead of just 'scale now, patch later.' 🤖 The only thing larger than their server farms is their #audacity in claiming they can teach anybody about #security and #privacy. 😂
https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/ #Correctness #HackerNews #ngated
C and C++ Prioritize Performance over Correctness (2023)
@geopolitics @politics
@society @education
via @Daniele1919
https://mastodon.social/@Daniele1919/114036095298614027
Hardly with #wokeism, #political in-#correctness, #velvet-gloving, #idiocy-protectionism, #hamas-apologism, and likes having invaded all #EU politics.
A #strong #alpha #dictator #philospher is not on the horizon (#Macron is an exception).
#Educate yourself. Grow your #consciousness. Become #alpha.
A correct answer is like an affectionate kiss.
[Eine richtige Antwort ist wie ein lieblicher Kuß.]
Johann Wolfgang von Goethe (1749-1832) German poet, statesman, scientist
Sprüche in Prosa: Maximen und Reflexionen [Proverbs in Prose: Maxims and Reflections] (1833) [tr. Mann (1948)]
Sourcing, notes, alternate translations: wist.info/goethe-johann/38240/
#quote #quotes #quotation #accomplishment #answer #correctness #kiss #pleasure #solution
#RemiPommarel found and fixed a bug/regression in a recent change someone had added to @batadv in the #Linux #kernel. One take home message from Remi:
"On a side note, I am all about #hardening and #MemorySafety stuff but if that means impacting readability and spending more time trying to please the tool than thinking about the #correctness of the code change, that's where we end up converting a perfectly fine #code into a logically flawed one."
(hash tags added by me)
#Velvet #Gloves are used to handle fragile materials.
Political #correctness is a velvet glove for the #feeble masses.
Feeble #specimens unable to handle their environment assuredly faint into extinction.
#againstdarkmanners #consciousnessevolution
@society @education
@rants
If you work with #LLVM IR and require type information a friend has just published the initial release of the library llvm-dimeta. it uses LLVM debug information to restore type information for your program's allocations.
Check it out at https://github.com/ahueck/llvm-dimeta
#software #softwareengineering #clang #compiler #correctness
My #computing is far too important for me to be pacified by mere #MemorySafety. I demand actual #correctness.
#coauthor #checking #calculation #correctness #already #know #phdstudent #doctoratestudent #phd #doctorate #motivation #meme #memes #phdmotivation #phdmeme #phdmemes #phdlife #phdstudentlife #phdtroll #doctoratemotivation #doctoratememe #doctoratememes #doctoratelife #doctoratestudentlife #doctoratetroll
If you are curious about our #unittest approach with #OMPT for #OpenMP implementations (at least the one in #ROCm ) check out our paper on it at #sc24 !
I will be talking about it at the #Correctness workshop.
https://sc24.conference-program.com/presentation/?id=ws_corr103&sess=sess759
A while a go I started working on a modal semantics for defining errors in distributed computing via types. The results have now appeared in a chapter for a volume dedicated to one my PhD mentors and teacher Göran Sundholm. The actual formalism is a bit far away from the tons of things I learned from him, but it touches on the issues of correctness and errors in proofs part of his philosophical research.
#proofs #computing #errors #correctness
https://link.springer.com/chapter/10.1007/978-3-031-52411-0_11
